:: Introduction to Lattice Theory
::  by Stanis{\l}aw \.Zukowski
::
:: Received April 14, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies STRUCT_0, BINOP_1, XBOOLE_0, ZFMISC_1, SUBSET_1, EQREL_1,
      FUNCT_1, PBOOLE, XXREAL_2, CAT_1, LATTICES, CARD_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, CARD_1, STRUCT_0, BINOP_1;
 constructors BINOP_1, STRUCT_0;
 registrations XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, STRUCT_0;
 requirements SUBSET, BOOLE, NUMERALS;
 definitions STRUCT_0;
 theorems ZFMISC_1, SUBSET_1, STRUCT_0;

begin

definition
  struct(1-sorted) /\-SemiLattStr (# carrier -> set, L_meet -> BinOp of the
    carrier #);
end;

definition
  struct (1-sorted) \/-SemiLattStr (# carrier -> set, L_join -> BinOp of the
    carrier #);
end;

definition
  struct (/\-SemiLattStr,\/-SemiLattStr) LattStr (# carrier -> set, L_join,
    L_meet -> BinOp of the carrier #);
end;

registration
  let D be non empty set, u be BinOp of D;
  cluster \/-SemiLattStr (# D, u #) -> non empty;
  coherence;
  cluster /\-SemiLattStr (# D, u #) -> non empty;
  coherence;
end;

registration
  let D be non empty set, u,n be BinOp of D;
  cluster LattStr (# D, u, n #) -> non empty;
  coherence;
end;

registration
  cluster 1-element strict for \/-SemiLattStr;
  existence
  proof
    set u = the BinOp of bool {};
    take L =  \/-SemiLattStr (# bool {}, u #);
    thus thesis by STRUCT_0:def 19,ZFMISC_1:1;
  end;
  cluster 1-element strict for /\-SemiLattStr;
  existence
  proof
    set u = the BinOp of bool {};
    take L = /\-SemiLattStr (# bool {}, u #);
    thus thesis by STRUCT_0:def 19,ZFMISC_1:1;
  end;
  cluster 1-element strict for LattStr;
  existence
  proof
    set u = the BinOp of bool {};
    take L = LattStr (# bool {}, u, u #);
    thus thesis by STRUCT_0:def 19,ZFMISC_1:1;
  end;
end;

definition
  let G be non empty \/-SemiLattStr, p, q be Element of G;
  func p"\/"q -> Element of G equals
  (the L_join of G).(p,q);
  coherence;
end;

definition
  let G be non empty /\-SemiLattStr, p, q be Element of G;
  func p"/\"q -> Element of G equals
  (the L_meet of G).(p,q);
  coherence;
end;

definition
  let G be non empty \/-SemiLattStr, p, q be Element of G;
  pred p [= q means
  :Def3:
  p"\/"q = q;
end;

Lm1: for uu,nn being BinOp of bool {}, x,y being Element of LattStr(#bool {},
  uu,nn#) holds x = y
proof
  let uu,nn be BinOp of bool {}, x,y be Element of LattStr(#bool {},uu,nn#);
  x = {};
  hence thesis;
end;

Lm2: for n being BinOp of bool {}, x,y being Element of \/-SemiLattStr (#bool
  {}, n#) holds x = y
proof
  let n be BinOp of bool {};
  let x,y be Element of \/-SemiLattStr (#bool {}, n#);
  x = {};
  hence thesis;
end;

Lm3: for n being BinOp of bool {}, x,y being Element of /\-SemiLattStr (#bool
  {}, n#) holds x = y
proof
  let n be BinOp of bool {};
  let x,y be Element of /\-SemiLattStr (#bool {}, n#);
  x = {};
  hence thesis;
end;

definition
  let IT be non empty \/-SemiLattStr;
  attr IT is join-commutative means
  :Def4:
  for a,b being Element of IT holds a "\/"b = b"\/"a;
  attr IT is join-associative means
  :Def5:
  for a,b,c being Element of IT holds a"\/"(b"\/"c) = (a"\/"b)"\/"c;
end;

definition
  let IT be non empty /\-SemiLattStr;
  attr IT is meet-commutative means
  :Def6:
  for a,b being Element of IT holds a "/\"b = b"/\"a;
  attr IT is meet-associative means
  :Def7:
  for a,b,c being Element of IT holds a"/\"(b"/\"c) = (a"/\"b)"/\"c;
end;

definition
  let IT be non empty LattStr;
  attr IT is meet-absorbing means
  :Def8:
  for a,b being Element of IT holds (a "/\"b)"\/"b = b;
  attr IT is join-absorbing means
  :Def9:
  for a,b being Element of IT holds a "/\"(a"\/"b)=a;
end;

definition
  let IT be non empty LattStr;
  attr IT is Lattice-like means
  :Def10:
  IT is join-commutative
  join-associative meet-absorbing meet-commutative meet-associative
  join-absorbing;
end;

registration
  cluster Lattice-like -> join-commutative join-associative meet-absorbing
    meet-commutative meet-associative join-absorbing for non empty LattStr;
  coherence by Def10;
  cluster join-commutative join-associative meet-absorbing meet-commutative
    meet-associative join-absorbing -> Lattice-like for non empty LattStr;
  coherence by Def10;
end;

registration
  cluster strict join-commutative join-associative for
non empty \/-SemiLattStr;
  existence
  proof
    set u = the BinOp of bool {};
    take GGj = \/-SemiLattStr(#bool {},u#);
    ( for x,y being Element of GGj holds x"\/"y = y"\/"x)& for x,y,z being
    Element of GGj holds x"\/"(y"\/"z) = (x"\/"y)"\/"z by Lm2;
    hence thesis by Def4,Def5;
  end;
  cluster strict meet-commutative meet-associative for
non empty /\-SemiLattStr;
  existence
  proof
    set u = the BinOp of bool {};
    take GGm = /\-SemiLattStr(#bool {},u#);
    ( for x,y being Element of GGm holds x"/\"y = y"/\"x)& for x,y,z being
    Element of GGm holds x"/\"(y"/\"z) = (x"/\"y)"/\"z by Lm3;
    hence thesis by Def6,Def7;
  end;
  cluster strict Lattice-like for non empty LattStr;
  existence
  proof
    set u = the BinOp of bool {};
    take GG = LattStr(#bool {},u,u#);
A1: ( for x,y being Element of GG holds (x"/\"y)"\/"y = y)& for x,y being
    Element of GG holds x"/\"y = y"/\"x by Lm1;
A2: ( for x,y,z being Element of GG holds x"/\"(y"/\"z) = (x"/\"y)"/\"z)&
    for x,y being Element of GG holds x"/\"(x"\/"y) = x by Lm1;
    ( for x,y being Element of GG holds x"\/"y = y"\/"x)& for x,y,z being
    Element of GG holds x"\/"(y"\/"z) = (x"\/"y)"\/"z by Lm1;
    then GG is join-commutative join-associative meet-absorbing
    meet-commutative meet-associative join-absorbing by A1,A2,Def4,Def5,Def6
,Def7,Def8,Def9;
    hence thesis;
  end;
end;

definition
  mode Lattice is Lattice-like non empty LattStr;
end;

definition
  let L be join-commutative non empty \/-SemiLattStr, a, b be Element of L;
  redefine func a"\/"b;
  commutativity by Def4;
end;

definition
  let L be meet-commutative non empty /\-SemiLattStr, a, b be Element of L;
  redefine func a"/\"b;
  commutativity by Def6;
end;

definition
  let IT be non empty LattStr;
  attr IT is distributive means
  :Def11:
  for a,b,c being Element of IT holds a "/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c);
end;

definition
  let IT be non empty LattStr;
  attr IT is modular means
  :Def12:
  for a,b,c being Element of IT st a [= c holds a"\/"(b"/\"c) = (a"\/"b)"/\"c;
end;

definition
  let IT be non empty /\-SemiLattStr;
  attr IT is lower-bounded means
  :Def13:
  ex c being Element of IT st for a
  being Element of IT holds c"/\"a = c & a"/\"c = c;
end;

definition
  let IT be non empty \/-SemiLattStr;
  attr IT is upper-bounded means
  :Def14:
  ex c being Element of IT st for a
  being Element of IT holds c"\/"a = c & a"\/"c = c;
end;

Lm4: for n,u being BinOp of bool {} holds LattStr (#bool {},n,u#) is Lattice
proof
  let n,u be BinOp of bool {};
  set G = LattStr (#bool {},n,u#);
  for x,y,z being Element of G holds x"\/"(y"\/"z) = (x"\/"y)"\/"z by Lm1;
  then
A1: G is join-associative by Def5;
  for x,y being Element of G holds (x"/\"y)"\/"y = y by Lm1;
  then
A2: G is meet-absorbing by Def8;
  for x,y being Element of G holds x"/\"(x"\/"y) = x by Lm1;
  then
A3: G is join-absorbing by Def9;
  for x,y,z being Element of G holds x"/\"(y"/\"z) = (x"/\"y)"/\"z by Lm1;
  then
A4: G is meet-associative by Def7;
  for x,y being Element of G holds x"/\"y = y"/\"x by Lm1;
  then
A5: G is meet-commutative by Def6;
  for x,y being Element of G holds x"\/"y = y"\/"x by Lm1;
  then G is join-commutative by Def4;
  hence thesis by A1,A2,A5,A4,A3;
end;

registration
  cluster strict distributive lower-bounded upper-bounded modular for Lattice;
  existence
  proof
    set uu = the BinOp of bool {};
    set GG=LattStr(#bool {},uu,uu#);
    reconsider GG as Lattice by Lm4;
    reconsider 0GG={}, D = {} as Element of GG by ZFMISC_1:def 1;
    for x being Element of GG holds 0GG"/\"x = 0GG & x"/\"0GG = 0GG;
    then
A1: GG is lower-bounded by Def13;
    for x being Element of GG holds D"\/"x = D & x"\/"D = D;
    then
A2: GG is upper-bounded by Def14;
    for x,y,z being Element of GG holds x"/\"(y"\/"z) = (x"/\"y)"\/"(x"/\"
    z) by Lm1;
    then
A3: GG is distributive by Def11;
    for x,y,z being Element of GG holds x [= z implies x"\/"(y"/\"z) = (x
    "\/"y)"/\"z by Lm1;
    then GG is modular by Def12;
    hence thesis by A1,A3,A2;
  end;
end;

definition
  mode D_Lattice is distributive Lattice;
  mode M_Lattice is modular Lattice;
  mode 0_Lattice is lower-bounded Lattice;
  mode 1_Lattice is upper-bounded Lattice;
end;

Lm5: for n,u being BinOp of bool {} holds LattStr (#bool {},n,u#) is 0_Lattice
proof
  let n,u be BinOp of bool {};
  set G = LattStr (#bool {},n,u#);
  reconsider G as Lattice by Lm4;
  reconsider D={} as Element of G by ZFMISC_1:def 1;
  for x being Element of G holds D"/\"x = D & x"/\"D = D;
  hence thesis by Def13;
end;

Lm6: for n,u being BinOp of bool {} holds LattStr (#bool {},n,u#) is 1_Lattice
proof
  let n,u be BinOp of bool {};
  set G = LattStr (#bool {},n,u#);
  reconsider G as Lattice by Lm4;
  reconsider D={} as Element of G by ZFMISC_1:def 1;
  for x being Element of G holds D"\/"x = D & x"\/"D = D;
  hence thesis by Def14;
end;

definition
  let IT be non empty LattStr;
  attr IT is bounded means
  :Def15:
  IT is lower-bounded upper-bounded;
end;

registration
  cluster lower-bounded upper-bounded -> bounded for non empty LattStr;
  coherence by Def15;
  cluster bounded -> lower-bounded upper-bounded for non empty LattStr;
  coherence by Def15;
end;

registration
  cluster bounded strict for Lattice;
  existence
  proof
    set uu = the BinOp of bool {};
    set G=LattStr(#bool {},uu,uu#);
    reconsider G as Lattice by Lm4;
    G is 0_Lattice & G is 1_Lattice by Lm5,Lm6;
    hence thesis;
  end;
end;

definition
  mode 01_Lattice is bounded Lattice;
end;

definition
  let L be non empty /\-SemiLattStr;
  assume
A1: L is lower-bounded;
  func Bottom L -> Element of L means
  :Def16:
  for a being Element of L holds it "/\" a = it & a "/\" it = it;
  existence by A1,Def13;
  uniqueness
  proof
    let c1,c2 be Element of L such that
A2: for a being Element of L holds c1"/\"a = c1 & a"/\"c1 = c1 and
A3: for a being Element of L holds c2"/\"a = c2 & a"/\"c2 = c2;
    thus c1 = c2"/\"c1 by A2
      .= c2 by A3;
  end;
end;

definition
  let L be non empty \/-SemiLattStr;
  assume
A1: L is upper-bounded;
  func Top L -> Element of L means
  :Def17:
  for a being Element of L holds it "\/" a = it & a "\/" it = it;
  existence by A1,Def14;
  uniqueness
  proof
    let c1,c2 be Element of L such that
A2: for a being Element of L holds c1"\/"a = c1 & a"\/"c1 = c1 and
A3: for a being Element of L holds c2"\/"a = c2 & a"\/"c2 = c2;
    thus c1 = c2"\/"c1 by A2
      .= c2 by A3;
  end;
end;

definition
  let L be non empty LattStr, a, b be Element of L;
  pred a is_a_complement_of b means
  :Def18:
  a"\/"b = Top L & b"\/"a = Top L & a"/\"b = Bottom L & b"/\"a = Bottom L;
end;

definition
  let IT be non empty LattStr;
  attr IT is complemented means
  :Def19:
  for b being Element of IT ex a being Element of IT st a is_a_complement_of b;
end;

registration
  cluster bounded complemented strict for Lattice;
  existence
  proof
    set n = the BinOp of bool {};
    reconsider GG = LattStr (#bool {},n,n#) as strict Lattice by Lm4;
    take GG;
    GG is 0_Lattice & GG is 1_Lattice by Lm5,Lm6;
    hence GG is bounded;
    thus GG is complemented
    proof
      set a = the Element of GG;
      let b be Element of GG;
      take a;
      thus a"\/"b = Top GG & b"\/"a = Top GG by Lm1;
      thus a"/\"b = Bottom GG & b"/\"a = Bottom GG by Lm1;
    end;
    thus thesis;
  end;
end;

definition
  mode C_Lattice is complemented 01_Lattice;
end;

definition
  let IT be non empty LattStr;
  attr IT is Boolean means
  :Def20:
  IT is bounded complemented distributive;
end;

registration
  cluster Boolean -> bounded complemented distributive for non empty LattStr;
  coherence by Def20;
  cluster bounded complemented distributive -> Boolean for non empty LattStr;
  coherence by Def20;
end;

registration
  cluster Boolean strict for Lattice;
  existence
  proof
    set n = the BinOp of bool {};
    reconsider G = LattStr (#bool {},n,n#) as strict Lattice by Lm4;
A1: G is complemented
    proof
      let b be Element of G;
      take b;
      thus b"\/"b = Top G & b"\/"b = Top G by Lm1;
      thus b"/\"b = Bottom G & b"/\"b = Bottom G by Lm1;
    end;
    G is 0_Lattice & G is 1_Lattice by Lm5,Lm6;
    then reconsider G as C_Lattice by A1;
    for x,y,z being Element of G holds x"/\"(y"\/"z) = (x"/\"y)"\/"(x"/\"z
    ) by Lm1;
    then G is distributive by Def11;
    hence thesis;
  end;
end;

definition
  mode B_Lattice is Boolean Lattice;
end;

registration
 let L be meet-absorbing join-absorbing meet-commutative non empty LattStr,
  a be Element of L;
 reduce a "\/" a to a;
 reducibility
proof
  thus a"\/"a = ( a "/\" ( a"\/"a ) ) "\/" a by Def9
    .= a by Def8;
end;
end;

registration
  let L be meet-absorbing join-absorbing meet-commutative non empty LattStr,
  a be Element of L;
 reduce a "/\" a to a;
 reducibility
proof
  a"/\"( a"\/"a ) = a by Def9;
  hence thesis;
end;
end;

canceled 2;

theorem Th3:
  for L being Lattice holds (for a,b,c being Element of L holds a
  "/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c)) iff for a,b,c being Element of L holds a
  "\/"(b"/\"c) = (a"\/"b)"/\"(a"\/"c)
proof
  let L be Lattice;
  hereby
    assume
A1: for a,b,c be Element of L holds a"/\"(b"\/"c)=(a"/\"b)"\/"(a"/\"c);
    let a,b,c be Element of L;
    thus a"\/"(b"/\"c)=(a"\/"(c"/\"a))"\/"(c"/\"b) by Def8
      .=a"\/"((c"/\"a)"\/"(c"/\"b)) by Def5
      .=a"\/"((a"\/"b)"/\"c) by A1
      .=((a"\/"b)"/\"a)"\/"((a"\/"b)"/\"c) by Def9
      .=(a"\/"b)"/\"(a"\/"c) by A1;
  end;
  assume
A2: for a,b,c be Element of L holds a"\/"(b"/\"c)=(a"\/"b)"/\"(a"\/"c);
  let a,b,c be Element of L;
  thus a"/\"(b"\/"c)=(a"/\"(c"\/"a))"/\"(c"\/"b) by Def9
    .=a"/\"((c"\/"a)"/\"(c"\/"b)) by Def7
    .=a"/\"((a"/\"b)"\/"c) by A2
    .=((a"/\"b)"\/"a)"/\"((a"/\"b)"\/"c) by Def8
    .=(a"/\"b)"\/"(a"/\"c) by A2;
end;

theorem Th4:
  for L being meet-absorbing join-absorbing non empty LattStr, a
  , b being Element of L holds a [= b iff a"/\"b = a
proof
  let L be meet-absorbing join-absorbing non empty LattStr, a, b be Element
  of L;
  a [= b iff a"\/"b = b by Def3;
  hence thesis by Def8,Def9;
end;

theorem Th5:
  for L being meet-absorbing join-absorbing join-associative
meet-commutative non empty LattStr, a, b being Element of L holds a [= a"\/"b
proof
  let L be meet-absorbing join-absorbing join-associative meet-commutative
  non empty LattStr, a, b be Element of L;
  thus a"\/"( a"\/"b) = (a"\/"a)"\/"b by Def5
    .= a"\/"b;
end;

theorem Th6:
  for L being meet-absorbing meet-commutative non empty LattStr,
  a, b being Element of L holds a"/\"b [= a
proof
  let L be meet-absorbing meet-commutative non empty LattStr, a, b be
  Element of L;
  thus ( a"/\"b )"\/"a = a by Def8;
end;

definition
  let L be meet-absorbing join-absorbing meet-commutative non empty LattStr,
  a, b be Element of L;
  redefine pred a [= b;
  reflexivity
  proof
    let a be Element of L;
    thus a"\/"a = a;
  end;
end;

theorem
  for L being join-associative non empty \/-SemiLattStr, a, b, c being
  Element of L holds a [= b & b [= c implies a [= c
proof
  let L be join-associative non empty \/-SemiLattStr, a, b, c be Element of
  L;
  assume a"\/"b = b & b"\/"c = c;
  hence a"\/"c = c by Def5;
end;

theorem Th8:
  for L being join-commutative non empty \/-SemiLattStr, a, b
  being Element of L holds a [= b & b [= a implies a=b
proof
  let L be join-commutative non empty \/-SemiLattStr, a, b be Element of L;
  assume a"\/"b = b & b"\/"a =a;
  hence thesis;
end;

theorem Th9:
  for L being meet-absorbing join-absorbing meet-associative non
empty LattStr, a, b, c being Element of L holds a [= b implies a"/\"c [= b"/\"
  c
proof
  let L be meet-absorbing join-absorbing meet-associative non empty LattStr,
  a, b, c be Element of L;
  assume a [= b;
  hence (a"/\"c)"\/"(b"/\"c) = ((a"/\"b)"/\"c)"\/"(b"/\"c) by Th4
    .= (a"/\"(b"/\"c))"\/"(b"/\"c) by Def7
    .= b"/\"c by Def8;
end;

theorem
  for L being Lattice holds (for a,b,c being Element of L holds (a"/\"b)
  "\/"(b"/\"c)"\/"(c"/\"a) = (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a)) implies L is
  distributive
proof
  let L be Lattice;
  assume
A1: for a,b,c being Element of L holds (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a)
  = (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a);
A2: now
    let a,b,c be Element of L;
    assume
A3: c [= a;
    thus a"/\"(b"\/"c) = (b"\/"c)"/\"(a"/\"(a"\/"b)) by Def9
      .= (a"\/"b)"/\"((b"\/"c)"/\"a) by Def7
      .= (a"\/"b)"/\"((b"\/"c)"/\"(c"\/"a)) by A3,Def3
      .= (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a) by Def7
      .= (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a) by A1
      .= (a"/\"b)"\/"((b"/\"c)"\/"(c"/\"a)) by Def5
      .= (a"/\"b)"\/"((b"/\"c)"\/"c) by A3,Th4
      .= (a"/\"b)"\/"c by Def8;
  end;
  let a,b,c be Element of L;
B4: ((a"/\"b)"\/"(c"/\"a))"\/"a = (a"/\"b)"\/"((c"/\"a)"\/"a) by Def5
    .= (a"/\"b)"\/"a by Def8
    .= a by Def8;
  thus a"/\"(b"\/"c) = (a"/\"(c"\/"a))"/\"(b"\/"c) by Def9
    .= a"/\"((c"\/"a)"/\"(b"\/"c)) by Def7
    .= (a"/\"(a"\/"b))"/\"((c"\/"a)"/\"(b"\/"c)) by Def9
    .= a"/\"((a"\/"b)"/\"((b"\/"c)"/\"(c"\/"a))) by Def7
    .= a"/\"((a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a)) by Def7
    .= a"/\"((b"/\"c)"\/"(a"/\"b)"\/"(c"/\"a)) by A1
    .= a"/\"((b"/\"c)"\/"((a"/\"b)"\/"(c"/\"a))) by Def5
    .= (a"/\"(b"/\"c))"\/"((a"/\"b)"\/"(c"/\"a)) by A2,B4,Def3
    .= (a"/\"b"/\"c)"\/"((a"/\"b)"\/"(c"/\"a)) by Def7
    .= ((a"/\"b"/\"c)"\/"(a"/\"b))"\/"(c"/\"a) by Def5
    .= (a"/\"b)"\/"(a"/\"c) by Def8;
end;

reserve L for D_Lattice;
reserve a, b, c for Element of L;

theorem Th11:
  a"\/"(b"/\"c) = (a"\/"b)"/\"(a"\/"c)
proof
  for a,b,c holds a"/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c) by Def11;
  hence thesis by Th3;
end;

theorem Th12:
  c"/\"a = c"/\"b & c"\/"a = c"\/"b implies a=b
proof
  assume that
A1: c"/\"a = c"/\"b and
A2: c"\/"a = c"\/"b;
  thus a = a"/\"( c"\/"a ) by Def9
    .= ( b"/\"c )"\/"( b"/\"a ) by A1,A2,Def11
    .= b"/\"( c"\/"a ) by Def11
    .= b by A2,Def9;
end;

theorem
  (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a) = (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a)
proof
  thus (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a) = (((a"\/"b)"/\"(b"\/"c))"/\"c)"\/"(((
  a"\/"b)"/\"(b"\/"c))"/\"a) by Def11
    .= ((a"\/"b)"/\"((b"\/"c)"/\"c))"\/"(((a"\/"b)"/\"(b"\/"c))"/\"a) by Def7
    .= ((a"\/"b)"/\"c)"\/"(a"/\"((a"\/"b)"/\"(b"\/"c))) by Def9
    .= ((a"\/"b)"/\"c)"\/"((a"/\"(a"\/"b))"/\"(b"\/"c)) by Def7
    .= (c"/\"(a"\/"b))"\/"(a"/\"(b"\/"c)) by Def9
    .= ((c"/\"a)"\/"(c"/\"b))"\/"(a"/\"(b"\/"c)) by Def11
    .= ((a"/\"b)"\/"(c"/\"a))"\/"((c"/\"a)"\/"(b"/\"c)) by Def11
    .= (a"/\"b)"\/"((c"/\"a)"\/"((c"/\"a)"\/"(b"/\"c))) by Def5
    .= (a"/\"b)"\/"(((c"/\"a)"\/"(c"/\"a))"\/"(b"/\"c)) by Def5
    .= (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a) by Def5;
end;

registration
  cluster distributive -> modular for Lattice;
  coherence
  proof
    let L be Lattice;
    assume
A1: L is distributive;
    let a,b,c be Element of L;
    assume a"\/"c = c;
    hence a"\/"(b"/\"c) = (a"\/"b)"/\"c by A1,Th11;
  end;
end;

registration
  let L be 0_Lattice, a be Element of L;
 reduce Bottom L "\/" a to a;
 reducibility
proof
  thus Bottom L"\/"a = ( Bottom L"/\"a )"\/"a by Def16
    .= a by Def8;
end;
 reduce Bottom L "/\" a to Bottom L;
 reducibility by Def16;
end;

theorem
  for L being 0_Lattice, a being Element of L holds Bottom L "\/" a = a;

theorem
  for L being 0_Lattice, a being Element of L holds Bottom L "/\" a = Bottom L;

theorem Th16:
  for L being 0_Lattice, a being Element of L holds Bottom L [= a
proof
  let L be 0_Lattice, a be Element of L;
  Bottom L [= Bottom L "\/" a by Th5;
  hence thesis;
end;

registration
  let L be 1_Lattice, a be Element of L;
 reduce Top L"/\"a to a;
 reducibility
proof
  thus Top L"/\"a = ( Top L"\/"a )"/\"a by Def17
    .= a by Def9;
end;
 reduce Top L"\/"a to Top L;
 reducibility by Def17;
end;

theorem
  for L being 1_Lattice, a being Element of L holds Top L"/\"a = a;

theorem
  for L being 1_Lattice, a being Element of L holds Top L"\/"a = Top L;

theorem
  for L being 1_Lattice, a being Element of L holds a [= Top L
proof
  let L be 1_Lattice, a be Element of L;
  Top L"/\"a [= Top L by Th6;
  hence thesis;
end;

definition
  let L be non empty LattStr, x be Element of L;
  assume
A1: L is complemented D_Lattice;
  func x` -> Element of L means
  :Def21:
  it is_a_complement_of x;
  existence by A1,Def19;
  uniqueness
  proof
    let a,b be Element of L such that
A2: a is_a_complement_of x and
A3: b is_a_complement_of x;
A4: x"\/"b = Top L & x"/\"b = Bottom L by A3,Def18;
    x"\/"a = Top L & x"/\"a = Bottom L by A2,Def18;
    hence thesis by A1,A4,Th12;
  end;
end;

reserve L for B_Lattice;
reserve a, b for Element of L;

theorem Th20:
  a`"/\"a = Bottom L
proof
  a` is_a_complement_of a by Def21;
  hence thesis by Def18;
end;

theorem Th21:
  a`"\/"a = Top L
proof
  a` is_a_complement_of a by Def21;
  hence thesis by Def18;
end;

registration let L,a;
 reduce a`` to a;
 reducibility
proof
  a` is_a_complement_of a by Def21;
  then
A1: a"\/"a` =Top L & a "/\"a`= Bottom L by Def18;
  a`` is_a_complement_of a` by Def21;
  then a``"\/"a` = Top L & a``"/\"a` = Bottom L by Def18;
  hence thesis by A1,Th12;
end;
end;

theorem
  a`` = a;

theorem Th23:
  ( a"/\"b )` = a`"\/" b`
proof
A1: (a`"\/"b`)"/\"(a"/\"b) = ((a`"\/"b`)"/\"a)"/\"b by Def7
    .= ((a`"/\"a)"\/"(b`"/\"a))"/\"b by Def11
    .= (Bottom L"\/"(b`"/\"a))"/\"b by Th20
    .= (b"/\"b`)"/\"a by Def7
    .= Bottom L"/\"a by Th20
    .= Bottom L;
  (a`"\/"b`)"\/"(a"/\"b) = a`"\/"(b`"\/"(a"/\"b)) by Def5
    .= a`"\/"((b`"\/"a)"/\"(b`"\/"b)) by Th11
    .= a`"\/"((b`"\/"a)"/\"Top L) by Th21
    .= b`"\/"(a"\/"a`) by Def5
    .= b`"\/"Top L by Th21
    .= Top L;
  then a`"\/"b` is_a_complement_of a"/\"b by A1,Def18;
  hence thesis by Def21;
end;

theorem
  ( a"\/"b )` = a`"/\" b`
proof
  thus (a"\/"b)` = (a``"\/"b``)`
    .= (a`"/\"b`)`` by Th23
    .= a`"/\"b`;
end;

theorem Th25:
  b"/\"a = Bottom L iff b [= a`
proof
  thus b"/\"a = Bottom L implies b [= a`
  proof
    assume
A1: b"/\"a = Bottom L;
    b = b"/\"Top L
      .= b"/\"(a"\/"a`) by Th21
      .= Bottom L"\/"(b"/\"a`) by A1,Def11
      .= b"/\"a`;
    then b"\/"a` = a` by Def8;
    hence thesis by Def3;
  end;
  thus thesis
  proof
    assume b [= a`;
    then b"/\"a [= a`"/\"a by Th9;
    then
A2: b"/\"a [= Bottom L by Th20;
    Bottom L [= b"/\"a by Th16;
    hence thesis by A2,Th8;
  end;
end;

theorem
  a [= b implies b` [= a`
proof
  assume a [= b;
  then b`"/\"a [= b`"/\"b by Th9;
  then
A1: b`"/\"a [= Bottom L by Th20;
  Bottom L [= b`"/\"a by Th16;
  then b `"/\"a = Bottom L by A1,Th8;
  hence thesis by Th25;
end;

begin :: Addenda
:: missing, 2009.07.28, A.T.

definition let L be Lattice, S be Subset of L;
 attr S is initial means
:Def22:  for p,q being Element of L st p [= q & q in S holds p in S;
 attr S is final means
:Def23:  for p,q being Element of L st p [= q & p in S holds q in S;
 attr S is meet-closed means
  for p,q being Element of L st p in S & q in S holds p "/\" q in S;
 attr S is join-closed means
  for p,q being Element of L st p in S & q in S holds p "\/" q in S;
end;

registration let L be Lattice;
 cluster [#]L -> initial final non empty;
 coherence
  proof
   thus [#]L is initial proof let p,q be Element of L;
     thus thesis;
    end;
   thus [#]L is final proof let p,q be Element of L;
     thus thesis;
    end;
   thus [#]L is non empty;
  end;
end;

registration let L be Lattice;
 cluster initial final non empty for Subset of L;
 existence
  proof
   take [#]L;
   thus thesis;
  end;
 cluster empty -> initial final for Subset of L;
 coherence
  proof let S be Subset of L;
   assume
A1:  S is empty;
   thus S is initial proof let p be Element of L;
     thus thesis by A1;
    end;
   let p be Element of L;
   thus thesis by A1;
  end;
 cluster initial -> meet-closed for Subset of L;
 coherence
  proof let S be Subset of L such that
A2:  S is initial;
   let p,q be Element of L such that p in S and
A3: q in S;
   thus p "/\" q in S by A2,A3,Def22,Th6;
  end;
 cluster final -> join-closed for Subset of L;
 coherence
  proof let S be Subset of L such that
A4:  S is final;
   let p,q be Element of L such that p in S and
A5: q in S;
   thus p "\/" q in S by A4,A5,Def23,Th5;
  end;
end;

theorem
 for L being Lattice, S being initial final non empty Subset of L
   holds S = [#]L
 proof let L be Lattice, S be initial final non empty Subset of L;
   consider p being Element of L such that
A1:  p in S by SUBSET_1:4;
   for x being Element of L holds x in S iff x in [#]L
    proof let x be Element of L;
     thus x in S implies x in [#]L;
     assume x in [#]L;
A2:     x "/\" p in S by A1,Def22,Th6;
     thus x in S by A2,Def23,Th6;
    end;
  hence S = [#]L by SUBSET_1:3;
 end;