:: LATTICES semantic presentation

begin

definition
attrc1 is strict ;
struct /\-SemiLattStr  ->  1-sorted ;
aggr/\-SemiLattStr(# carrier, L_meet #) ->  /\-SemiLattStr ;
sel L_meet c1 ->  BinOp of the carrier of c1;
end;

definition
attrc1 is strict ;
struct \/-SemiLattStr  ->  1-sorted ;
aggr\/-SemiLattStr(# carrier, L_join #) ->  \/-SemiLattStr ;
sel L_join c1 ->  BinOp of the carrier of c1;
end;

definition
attrc1 is strict ;
struct LattStr  ->  /\-SemiLattStr , \/-SemiLattStr ;
aggrLattStr(# carrier, L_join, L_meet #) ->  LattStr ;
end;

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

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

registration
cluster1 -element strict for \/-SemiLattStr ;
existence
 ex b1 being \/-SemiLattStr st
( b1 is 1 -element & b1 is strict )
proof
set u = the BinOp of (bool {});
take L = \/-SemiLattStr(# (bool {}), the BinOp of (bool {}) #); ::_thesis: ( L is 1 -element & L is strict )
thus  ( L is 1 -element & L is strict ) by STRUCT_0:def_19, ZFMISC_1:1; ::_thesis: verum
end;
cluster1 -element strict for /\-SemiLattStr ;
existence
 ex b1 being /\-SemiLattStr st
( b1 is 1 -element & b1 is strict )
proof
set u = the BinOp of (bool {});
take L = /\-SemiLattStr(# (bool {}), the BinOp of (bool {}) #); ::_thesis: ( L is 1 -element & L is strict )
thus  ( L is 1 -element & L is strict ) by STRUCT_0:def_19, ZFMISC_1:1; ::_thesis: verum
end;
cluster1 -element strict for LattStr ;
existence
 ex b1 being LattStr st
( b1 is 1 -element & b1 is strict )
proof
set u = the BinOp of (bool {});
take L = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #); ::_thesis: ( L is 1 -element & L is strict )
thus  ( L is 1 -element & L is strict ) by STRUCT_0:def_19, ZFMISC_1:1; ::_thesis: verum
end;
end;

definition
let G be non empty \/-SemiLattStr ;
let p, q be Element of G;
funcp "\/" q ->  Element of G equals :: LATTICES:def 1
 the L_join of G . (p,q);
coherence
 the L_join of G . (p,q) is Element of G ;
end;

:: deftheorem  defines "\/" LATTICES:def_1_:_
 for G being non empty \/-SemiLattStr
for p, q being Element of G holds p "\/" q = the L_join of G . (p,q);

definition
let G be non empty /\-SemiLattStr ;
let p, q be Element of G;
funcp "/\" q ->  Element of G equals :: LATTICES:def 2
 the L_meet of G . (p,q);
coherence
 the L_meet of G . (p,q) is Element of G ;
end;

:: deftheorem  defines "/\" LATTICES:def_2_:_
 for G being non empty /\-SemiLattStr
for p, q being Element of G holds p "/\" q = the L_meet of G . (p,q);

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

:: deftheorem Def3 defines [= LATTICES:def_3_:_
 for G being non empty \/-SemiLattStr
for p, q being Element of G holds
( p [= q iff p "\/" q = q );

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

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

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

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

:: deftheorem Def4 defines join-commutative LATTICES:def_4_:_
 for IT being non empty \/-SemiLattStr holds
( IT is join-commutative iff for a, b being Element of IT holds a "\/" b = b "\/" a );

:: deftheorem Def5 defines join-associative LATTICES:def_5_:_
 for IT being non empty \/-SemiLattStr holds
( IT is join-associative iff for a, b, c being Element of IT holds a "\/" (b "\/" c) = (a "\/" b) "\/" c );

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

:: deftheorem Def6 defines meet-commutative LATTICES:def_6_:_
 for IT being non empty /\-SemiLattStr holds
( IT is meet-commutative iff for a, b being Element of IT holds a "/\" b = b "/\" a );

:: deftheorem Def7 defines meet-associative LATTICES:def_7_:_
 for IT being non empty /\-SemiLattStr holds
( IT is meet-associative iff for a, b, c being Element of IT holds a "/\" (b "/\" c) = (a "/\" b) "/\" c );

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

:: deftheorem Def8 defines meet-absorbing LATTICES:def_8_:_
 for IT being non empty LattStr holds
( IT is meet-absorbing iff for a, b being Element of IT holds (a "/\" b) "\/" b = b );

:: deftheorem Def9 defines join-absorbing LATTICES:def_9_:_
 for IT being non empty LattStr holds
( IT is join-absorbing iff for a, b being Element of IT holds a "/\" (a "\/" b) = a );

definition
let IT be non empty LattStr ;
attrIT is Lattice-like  means :Def10: :: LATTICES:def 10
( IT is join-commutative & IT is join-associative & IT is meet-absorbing & IT is meet-commutative & IT is meet-associative & IT is join-absorbing );
end;

:: deftheorem Def10 defines Lattice-like LATTICES:def_10_:_
 for IT being non empty LattStr holds
( IT is Lattice-like iff ( IT is join-commutative & IT is join-associative & IT is meet-absorbing & IT is meet-commutative & IT is meet-associative & IT is join-absorbing ) );

registration
cluster non empty Lattice-like  ->  non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing for LattStr ;
coherence
 for b1 being non empty LattStr st b1 is Lattice-like holds
( b1 is join-commutative & b1 is join-associative & b1 is meet-absorbing & b1 is meet-commutative & b1 is meet-associative & b1 is join-absorbing ) by Def10;
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing  ->  non empty Lattice-like for LattStr ;
coherence
 for b1 being non empty LattStr st b1 is join-commutative & b1 is join-associative & b1 is meet-absorbing & b1 is meet-commutative & b1 is meet-associative & b1 is join-absorbing holds
b1 is Lattice-like by Def10;
end;

registration
cluster non empty strict join-commutative join-associative for \/-SemiLattStr ;
existence
 ex b1 being non empty \/-SemiLattStr st
( b1 is strict & b1 is join-commutative & b1 is join-associative )
proof
set u = the BinOp of (bool {});
take GGj = \/-SemiLattStr(# (bool {}), the BinOp of (bool {}) #); ::_thesis: ( GGj is strict & GGj is join-commutative & GGj is join-associative )
 ( ( 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  ( GGj is strict & GGj is join-commutative & GGj is join-associative ) by Def4, Def5; ::_thesis: verum
end;
cluster non empty strict meet-commutative meet-associative for /\-SemiLattStr ;
existence
 ex b1 being non empty /\-SemiLattStr st
( b1 is strict & b1 is meet-commutative & b1 is meet-associative )
proof
set u = the BinOp of (bool {});
take GGm = /\-SemiLattStr(# (bool {}), the BinOp of (bool {}) #); ::_thesis: ( GGm is strict & GGm is meet-commutative & GGm is meet-associative )
 ( ( 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  ( GGm is strict & GGm is meet-commutative & GGm is meet-associative ) by Def6, Def7; ::_thesis: verum
end;
cluster non empty strict Lattice-like for LattStr ;
existence
 ex b1 being non empty LattStr st
( b1 is strict & b1 is Lattice-like )
proof
set u = the BinOp of (bool {});
take GG = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #); ::_thesis: ( GG is strict & GG is Lattice-like )
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 & GG is join-associative & GG is meet-absorbing & GG is meet-commutative & GG is meet-associative & GG is join-absorbing ) by A1, A2, Def4, Def5, Def6, Def7, Def8, Def9;
hence  ( GG is strict & GG is Lattice-like ) ; ::_thesis: verum
end;
end;

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

definition
let L be non empty join-commutative \/-SemiLattStr ;
let a, b be Element of L;
:: original: "\/"
redefine funca "\/" b ->  Element of L;
commutativity
 for a, b being Element of L holds a "\/" b = b "\/" a by Def4;
end;

definition
let L be non empty meet-commutative /\-SemiLattStr ;
let a, b be Element of L;
:: original: "/\"
redefine funca "/\" b ->  Element of L;
commutativity
 for a, b being Element of L holds a "/\" b = b "/\" a by Def6;
end;

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

:: deftheorem Def11 defines distributive LATTICES:def_11_:_
 for IT being non empty LattStr holds
( IT is distributive iff for a, b, c being Element of IT holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) );

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

:: deftheorem Def12 defines modular LATTICES:def_12_:_
 for IT being non empty LattStr holds
( IT is modular iff for a, b, c being Element of IT st a [= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c );

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

:: deftheorem Def13 defines lower-bounded LATTICES:def_13_:_
 for IT being non empty /\-SemiLattStr holds
( IT is lower-bounded iff ex c being Element of IT st
for a being Element of IT holds
( c "/\" a = c & a "/\" c = c ) );

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

:: deftheorem Def14 defines upper-bounded LATTICES:def_14_:_
 for IT being non empty \/-SemiLattStr holds
( IT is upper-bounded iff ex c being Element of IT st
for a being Element of IT holds
( c "\/" a = c & a "\/" c = c ) );

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

registration
cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded for LattStr ;
existence
 ex b1 being Lattice st
( b1 is strict & b1 is distributive & b1 is lower-bounded & b1 is upper-bounded & b1 is modular )
proof
set uu = the BinOp of (bool {});
set GG = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #);
reconsider GG = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #) 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 st x [= z holds
x "\/" (y "/\" z) = (x "\/" y) "/\" z by Lm1;
then  GG is modular by Def12;
hence  ex b1 being Lattice st
( b1 is strict & b1 is distributive & b1 is lower-bounded & b1 is upper-bounded & b1 is modular ) by A1, A3, A2; ::_thesis: verum
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 {}); ::_thesis: LattStr(# (bool {}),n,u #) is 0_Lattice
set G = LattStr(# (bool {}),n,u #);
reconsider G = LattStr(# (bool {}),n,u #) 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  LattStr(# (bool {}),n,u #) is 0_Lattice by Def13; ::_thesis: verum
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 {}); ::_thesis: LattStr(# (bool {}),n,u #) is 1_Lattice
set G = LattStr(# (bool {}),n,u #);
reconsider G = LattStr(# (bool {}),n,u #) 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  LattStr(# (bool {}),n,u #) is 1_Lattice by Def14; ::_thesis: verum
end;

definition
let IT be non empty LattStr ;
attrIT is bounded  means :Def15: :: LATTICES:def 15
( IT is lower-bounded & IT is upper-bounded );
end;

:: deftheorem Def15 defines bounded LATTICES:def_15_:_
 for IT being non empty LattStr holds
( IT is bounded iff ( IT is lower-bounded & IT is upper-bounded ) );

registration
cluster non empty lower-bounded upper-bounded  ->  non empty bounded for LattStr ;
coherence
 for b1 being non empty LattStr st b1 is lower-bounded & b1 is upper-bounded holds
b1 is bounded by Def15;
cluster non empty bounded  ->  non empty lower-bounded upper-bounded for LattStr ;
coherence
 for b1 being non empty LattStr st b1 is bounded holds
( b1 is lower-bounded & b1 is upper-bounded ) by Def15;
end;

registration
cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like bounded for LattStr ;
existence
 ex b1 being Lattice st
( b1 is bounded & b1 is strict )
proof
set uu = the BinOp of (bool {});
set G = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #);
reconsider G = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #) as Lattice by Lm4;
 ( G is 0_Lattice & G is 1_Lattice ) by Lm5, Lm6;
hence  ex b1 being Lattice st
( b1 is bounded & b1 is strict ) ; ::_thesis: verum
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: :: LATTICES:def 16
 for a being Element of L holds
( it "/\" a = it & a "/\" it = it );
existence
 ex b1 being Element of L st
for a being Element of L holds
( b1 "/\" a = b1 & a "/\" b1 = b1 ) by A1, Def13;
uniqueness
 for b1, b2 being Element of L st ( for a being Element of L holds
( b1 "/\" a = b1 & a "/\" b1 = b1 ) ) & ( for a being Element of L holds
( b2 "/\" a = b2 & a "/\" b2 = b2 ) ) holds
b1 = b2
proof
let c1, c2 be Element of L; ::_thesis: ( ( for a being Element of L holds
( c1 "/\" a = c1 & a "/\" c1 = c1 ) ) & ( for a being Element of L holds
( c2 "/\" a = c2 & a "/\" c2 = c2 ) ) implies c1 = c2 )
assume 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 ) ; ::_thesis: c1 = c2
thus c1 = c2 "/\" c1 by A2
.= c2 by A3 ; ::_thesis: verum
end;
end;

:: deftheorem Def16 defines Bottom LATTICES:def_16_:_
 for L being non empty /\-SemiLattStr st L is lower-bounded holds
for b2 being Element of L holds
( b2 = Bottom L iff for a being Element of L holds
( b2 "/\" a = b2 & a "/\" b2 = b2 ) );

definition
let L be non empty \/-SemiLattStr ;
assume A1: L is upper-bounded ;
func Top L ->  Element of L means :Def17: :: LATTICES:def 17
 for a being Element of L holds
( it "\/" a = it & a "\/" it = it );
existence
 ex b1 being Element of L st
for a being Element of L holds
( b1 "\/" a = b1 & a "\/" b1 = b1 ) by A1, Def14;
uniqueness
 for b1, b2 being Element of L st ( for a being Element of L holds
( b1 "\/" a = b1 & a "\/" b1 = b1 ) ) & ( for a being Element of L holds
( b2 "\/" a = b2 & a "\/" b2 = b2 ) ) holds
b1 = b2
proof
let c1, c2 be Element of L; ::_thesis: ( ( for a being Element of L holds
( c1 "\/" a = c1 & a "\/" c1 = c1 ) ) & ( for a being Element of L holds
( c2 "\/" a = c2 & a "\/" c2 = c2 ) ) implies c1 = c2 )
assume 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 ) ; ::_thesis: c1 = c2
thus c1 = c2 "\/" c1 by A2
.= c2 by A3 ; ::_thesis: verum
end;
end;

:: deftheorem Def17 defines Top LATTICES:def_17_:_
 for L being non empty \/-SemiLattStr st L is upper-bounded holds
for b2 being Element of L holds
( b2 = Top L iff for a being Element of L holds
( b2 "\/" a = b2 & a "\/" b2 = b2 ) );

definition
let L be non empty LattStr ;
let a, b be Element of L;
preda is_a_complement_of b means :Def18: :: LATTICES:def 18
( a "\/" b = Top L & b "\/" a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L );
end;

:: deftheorem Def18 defines is_a_complement_of LATTICES:def_18_:_
 for L being non empty LattStr
for a, b being Element of L holds
( a is_a_complement_of b iff ( a "\/" b = Top L & b "\/" a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L ) );

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

:: deftheorem Def19 defines complemented LATTICES:def_19_:_
 for IT being non empty LattStr holds
( IT is complemented iff for b being Element of IT ex a being Element of IT st a is_a_complement_of b );

registration
cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like bounded complemented for LattStr ;
existence
 ex b1 being Lattice st
( b1 is bounded & b1 is complemented & b1 is strict )
proof
set n = the BinOp of (bool {});
reconsider GG = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #) as strict Lattice by Lm4;
take  GG ; ::_thesis: ( GG is bounded & GG is complemented & GG is strict )
 ( GG is 0_Lattice & GG is 1_Lattice ) by Lm5, Lm6;
hence  GG is bounded ; ::_thesis: ( GG is complemented & GG is strict )
thus  GG is complemented ::_thesis: GG is strict
proof
set a = the Element of GG;
let b be Element of GG; :: according to LATTICES:def_19 ::_thesis: ex a being Element of GG st a is_a_complement_of b
take  the Element of GG ; ::_thesis: the Element of GG is_a_complement_of b
thus  ( the Element of GG "\/" b = Top GG & b "\/" the Element of GG = Top GG ) by Lm1; :: according to LATTICES:def_18 ::_thesis: ( the Element of GG "/\" b = Bottom GG & b "/\" the Element of GG = Bottom GG )
thus  ( the Element of GG "/\" b = Bottom GG & b "/\" the Element of GG = Bottom GG ) by Lm1; ::_thesis: verum
end;
thus  GG is strict ; ::_thesis: verum
end;
end;

definition
mode C_Lattice is complemented 01_Lattice;
end;

definition
let IT be non empty LattStr ;
attrIT is Boolean  means :Def20: :: LATTICES:def 20
( IT is bounded & IT is complemented & IT is distributive );
end;

:: deftheorem Def20 defines Boolean LATTICES:def_20_:_
 for IT being non empty LattStr holds
( IT is Boolean iff ( IT is bounded & IT is complemented & IT is distributive ) );

registration
cluster non empty Boolean  ->  non empty distributive bounded complemented for LattStr ;
coherence
 for b1 being non empty LattStr st b1 is Boolean holds
( b1 is bounded & b1 is complemented & b1 is distributive ) by Def20;
cluster non empty distributive bounded complemented  ->  non empty Boolean for LattStr ;
coherence
 for b1 being non empty LattStr st b1 is bounded & b1 is complemented & b1 is distributive holds
b1 is Boolean by Def20;
end;

registration
cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Boolean for LattStr ;
existence
 ex b1 being Lattice st
( b1 is Boolean & b1 is strict )
proof
set n = the BinOp of (bool {});
reconsider G = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #) as strict Lattice by Lm4;
A1: G is complemented
proof
let b be Element of G; :: according to LATTICES:def_19 ::_thesis: ex a being Element of G st a is_a_complement_of b
take  b ; ::_thesis: b is_a_complement_of b
thus  ( b "\/" b = Top G & b "\/" b = Top G ) by Lm1; :: according to LATTICES:def_18 ::_thesis: ( b "/\" b = Bottom G & b "/\" b = Bottom G )
thus  ( b "/\" b = Bottom G & b "/\" b = Bottom G ) by Lm1; ::_thesis: verum
end;
 ( G is 0_Lattice & G is 1_Lattice ) by Lm5, Lm6;
then reconsider G = 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  ex b1 being Lattice st
( b1 is Boolean & b1 is strict ) ; ::_thesis: verum
end;
end;

definition
mode B_Lattice is Boolean Lattice;
end;

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

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

theorem :: LATTICES:1
canceled;

theorem :: LATTICES:2
canceled;

theorem Th3: :: LATTICES:3
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; ::_thesis: ( ( 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) )
hereby  ::_thesis: ( ( for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) ) implies for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) )
assume A1: for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) ; ::_thesis: for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)
let a, b, c be Element of L; ::_thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)
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 ; ::_thesis: verum
end;
assume A2: for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) ; ::_thesis: for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
let a, b, c be Element of L; ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
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 ; ::_thesis: verum
end;

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

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

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

definition
let L be non empty meet-commutative meet-absorbing join-absorbing LattStr ;
let a, b be Element of L;
:: original: [=
redefine preda [= b;
reflexivity
 for a being Element of L holds (L,b1,b1)
proof
let a be Element of L; ::_thesis: (L,a,a)
thus  a "\/" a = a ; :: according to LATTICES:def_3 ::_thesis: verum
end;
end;

theorem :: LATTICES:7
for L being non empty join-associative \/-SemiLattStr
for a, b, c being Element of L st a [= b & b [= c holds
a [= c
proof
let L be non empty join-associative \/-SemiLattStr ; ::_thesis: for a, b, c being Element of L st a [= b & b [= c holds
a [= c
let a, b, c be Element of L; ::_thesis: ( a [= b & b [= c implies a [= c )
assume  ( a "\/" b = b & b "\/" c = c ) ; :: according to LATTICES:def_3 ::_thesis: a [= c
hence  a "\/" c = c by Def5; :: according to LATTICES:def_3 ::_thesis: verum
end;

theorem Th8: :: LATTICES:8
for L being non empty join-commutative \/-SemiLattStr
for a, b being Element of L st a [= b & b [= a holds
a = b
proof
let L be non empty join-commutative \/-SemiLattStr ; ::_thesis: for a, b being Element of L st a [= b & b [= a holds
a = b
let a, b be Element of L; ::_thesis: ( a [= b & b [= a implies a = b )
assume  ( a "\/" b = b & b "\/" a = a ) ; :: according to LATTICES:def_3 ::_thesis: a = b
hence  a = b ; ::_thesis: verum
end;

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

theorem :: LATTICES:10
for L being Lattice st ( for a, b, c being Element of L holds ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) ) holds
L is distributive
proof
let L be Lattice; ::_thesis: ( ( 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 )
assume A1: for a, b, c being Element of L holds ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) ; ::_thesis: L is distributive
A2: now__::_thesis:_for_a,_b,_c_being_Element_of_L_st_c_[=_a_holds_
a_"/\"_(b_"\/"_c)_=_(a_"/\"_b)_"\/"_c
let a, b, c be Element of L; ::_thesis: ( c [= a implies a "/\" (b "\/" c) = (a "/\" b) "\/" c )
assume A3: c [= a ; ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" c
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 ; ::_thesis: verum
end;
let a, b, c be Element of L; :: according to LATTICES:def_11 ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
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 ; ::_thesis: verum
end;


theorem Th11: :: LATTICES:11
for L being D_Lattice
for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)
proof
let L be D_Lattice; ::_thesis: for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)
let a, b, c be Element of L; ::_thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)
 for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by Def11;
hence  a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) by Th3; ::_thesis: verum
end;

theorem Th12: :: LATTICES:12
for L being D_Lattice
for c, a, b being Element of L st c "/\" a = c "/\" b & c "\/" a = c "\/" b holds
a = b
proof
let L be D_Lattice; ::_thesis: for c, a, b being Element of L st c "/\" a = c "/\" b & c "\/" a = c "\/" b holds
a = b
let c, a, b be Element of L; ::_thesis: ( c "/\" a = c "/\" b & c "\/" a = c "\/" b implies a = b )
assume that
A1: c "/\" a = c "/\" b and
A2: c "\/" a = c "\/" b ; ::_thesis: a = 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 ; ::_thesis: verum
end;

theorem :: LATTICES:13
for L being D_Lattice
for a, b, c being Element of L holds ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) = ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a)
proof
let L be D_Lattice; ::_thesis: for a, b, c being Element of L holds ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) = ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a)
let a, b, c be Element of L; ::_thesis: ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) = ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a)
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 ; ::_thesis: verum
end;

registration
cluster non empty Lattice-like distributive  ->  modular for LattStr ;
coherence
 for b1 being Lattice st b1 is distributive holds
b1 is modular
proof
let L be Lattice; ::_thesis: ( L is distributive implies L is modular )
assume A1: L is distributive ; ::_thesis: L is modular
let a, b, c be Element of L; :: according to LATTICES:def_12 ::_thesis: ( a [= c implies a "\/" (b "/\" c) = (a "\/" b) "/\" c )
assume  a "\/" c = c ; :: according to LATTICES:def_3 ::_thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" c
hence  a "\/" (b "/\" c) = (a "\/" b) "/\" c by A1, Th11; ::_thesis: verum
end;
end;

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

theorem :: LATTICES:14
for L being 0_Lattice
for a being Element of L holds (Bottom L) "\/" a = a ;

theorem :: LATTICES:15
for L being 0_Lattice
for a being Element of L holds (Bottom L) "/\" a = Bottom L ;

theorem Th16: :: LATTICES:16
for L being 0_Lattice
for a being Element of L holds Bottom L [= a
proof
let L be 0_Lattice; ::_thesis: for a being Element of L holds Bottom L [= a
let a be Element of L; ::_thesis: Bottom L [= a
 Bottom L [= (Bottom L) "\/" a by Th5;
hence  Bottom L [= a ; ::_thesis: verum
end;

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

theorem :: LATTICES:17
for L being 1_Lattice
for a being Element of L holds (Top L) "/\" a = a ;

theorem :: LATTICES:18
for L being 1_Lattice
for a being Element of L holds (Top L) "\/" a = Top L ;

theorem :: LATTICES:19
for L being 1_Lattice
for a being Element of L holds a [= Top L
proof
let L be 1_Lattice; ::_thesis: for a being Element of L holds a [= Top L
let a be Element of L; ::_thesis: a [= Top L
 (Top L) "/\" a [= Top L by Th6;
hence  a [= Top L ; ::_thesis: verum
end;

definition
let L be non empty LattStr ;
let x be Element of L;
assume A1: L is complemented D_Lattice ;
funcx `  ->  Element of L means :Def21: :: LATTICES:def 21
it is_a_complement_of x;
existence
 ex b1 being Element of L st b1 is_a_complement_of x by A1, Def19;
uniqueness
 for b1, b2 being Element of L st b1 is_a_complement_of x & b2 is_a_complement_of x holds
b1 = b2
proof
let a, b be Element of L; ::_thesis: ( a is_a_complement_of x & b is_a_complement_of x implies a = b )
assume that
A2: a is_a_complement_of x and
A3: b is_a_complement_of x ; ::_thesis: a = b
A4: ( x "\/" b = Top L & x "/\" b = Bottom L ) by A3, Def18;
 ( x "\/" a = Top L & x "/\" a = Bottom L ) by A2, Def18;
hence  a = b by A1, A4, Th12; ::_thesis: verum
end;
end;

:: deftheorem Def21 defines ` LATTICES:def_21_:_
 for L being non empty LattStr
for x being Element of L st L is complemented D_Lattice holds
for b3 being Element of L holds
( b3 = x ` iff b3 is_a_complement_of x );


theorem Th20: :: LATTICES:20
for L being B_Lattice
for a being Element of L holds (a `) "/\" a = Bottom L
proof
let L be B_Lattice; ::_thesis: for a being Element of L holds (a `) "/\" a = Bottom L
let a be Element of L; ::_thesis: (a `) "/\" a = Bottom L
 a ` is_a_complement_of a by Def21;
hence  (a `) "/\" a = Bottom L by Def18; ::_thesis: verum
end;

theorem Th21: :: LATTICES:21
for L being B_Lattice
for a being Element of L holds (a `) "\/" a = Top L
proof
let L be B_Lattice; ::_thesis: for a being Element of L holds (a `) "\/" a = Top L
let a be Element of L; ::_thesis: (a `) "\/" a = Top L
 a ` is_a_complement_of a by Def21;
hence  (a `) "\/" a = Top L by Def18; ::_thesis: verum
end;

registration
let L be B_Lattice;
let a be Element of L;
reduce(a `) `  to a;
reducibility
 (a `) ` = a
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  (a `) ` = a by A1, Th12; ::_thesis: verum
end;
end;

theorem :: LATTICES:22
for L being B_Lattice
for a being Element of L holds (a `) ` = a ;

theorem Th23: :: LATTICES:23
for L being B_Lattice
for a, b being Element of L holds (a "/\" b) ` = (a `) "\/" (b `)
proof
let L be B_Lattice; ::_thesis: for a, b being Element of L holds (a "/\" b) ` = (a `) "\/" (b `)
let a, b be Element of L; ::_thesis: (a "/\" b) ` = (a `) "\/" (b `)
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  (a "/\" b) ` = (a `) "\/" (b `) by Def21; ::_thesis: verum
end;

theorem :: LATTICES:24
for L being B_Lattice
for a, b being Element of L holds (a "\/" b) ` = (a `) "/\" (b `)
proof
let L be B_Lattice; ::_thesis: for a, b being Element of L holds (a "\/" b) ` = (a `) "/\" (b `)
let a, b be Element of L; ::_thesis: (a "\/" b) ` = (a `) "/\" (b `)
thus (a "\/" b) ` = (((a `) `) "\/" ((b `) `)) `
.= (((a `) "/\" (b `)) `) ` by Th23
.= (a `) "/\" (b `) ; ::_thesis: verum
end;

theorem Th25: :: LATTICES:25
for L being B_Lattice
for b, a being Element of L holds
( b "/\" a = Bottom L iff b [= a ` )
proof
let L be B_Lattice; ::_thesis: for b, a being Element of L holds
( b "/\" a = Bottom L iff b [= a ` )
let b, a be Element of L; ::_thesis: ( b "/\" a = Bottom L iff b [= a ` )
thus  ( b "/\" a = Bottom L implies b [= a ` ) ::_thesis: ( b [= a ` implies b "/\" a = Bottom L )
proof
assume A1: b "/\" a = Bottom L ; ::_thesis: b [= a `
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  b [= a ` by Def3; ::_thesis: verum
end;
thus  ( b [= a ` implies b "/\" a = Bottom L ) ::_thesis: verum
proof
assume  b [= a ` ; ::_thesis: b "/\" a = Bottom L
then  b "/\" a [= (a `) "/\" a by Th9;
then A2: b "/\" a [= Bottom L by Th20;
 Bottom L [= b "/\" a by Th16;
hence  b "/\" a = Bottom L by A2, Th8; ::_thesis: verum
end;
end;

theorem :: LATTICES:26
for L being B_Lattice
for a, b being Element of L st a [= b holds
b ` [= a `
proof
let L be B_Lattice; ::_thesis: for a, b being Element of L st a [= b holds
b ` [= a `
let a, b be Element of L; ::_thesis: ( a [= b implies b ` [= a ` )
assume  a [= b ; ::_thesis: b ` [= a `
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  b ` [= a ` by Th25; ::_thesis: verum
end;

begin

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

:: deftheorem Def22 defines initial LATTICES:def_22_:_
 for L being Lattice
for S being Subset of L holds
( S is initial iff for p, q being Element of L st p [= q & q in S holds
p in S );

:: deftheorem Def23 defines final LATTICES:def_23_:_
 for L being Lattice
for S being Subset of L holds
( S is final iff for p, q being Element of L st p [= q & p in S holds
q in S );

:: deftheorem  defines meet-closed LATTICES:def_24_:_
 for L being Lattice
for S being Subset of L holds
( S is meet-closed iff for p, q being Element of L st p in S & q in S holds
p "/\" q in S );

:: deftheorem  defines join-closed LATTICES:def_25_:_
 for L being Lattice
for S being Subset of L holds
( S is join-closed iff for p, q being Element of L st p in S & q in S holds
p "\/" q in S );

registration
let L be Lattice;
cluster [#] L ->  non empty initial final ;
coherence
 ( [#] L is initial & [#] L is final & not [#] L is empty )
proof
thus  [#] L is initial ::_thesis: ( [#] L is final & not [#] L is empty )
proof
let p, q be Element of L; :: according to LATTICES:def_22 ::_thesis: ( p [= q & q in [#] L implies p in [#] L )
thus  ( p [= q & q in [#] L implies p in [#] L ) ; ::_thesis: verum
end;
thus  [#] L is final ::_thesis: not [#] L is empty
proof
let p, q be Element of L; :: according to LATTICES:def_23 ::_thesis: ( p [= q & p in [#] L implies q in [#] L )
thus  ( p [= q & p in [#] L implies q in [#] L ) ; ::_thesis: verum
end;
thus  not [#] L is empty ; ::_thesis: verum
end;
end;

registration
let L be Lattice;
cluster non empty initial final for M2( bool the carrier of L);
existence
 ex b1 being Subset of L st
( b1 is initial & b1 is final & not b1 is empty )
proof
take  [#] L ; ::_thesis: ( [#] L is initial & [#] L is final & not [#] L is empty )
thus  ( [#] L is initial & [#] L is final & not [#] L is empty ) ; ::_thesis: verum
end;
cluster empty  ->  initial final for M2( bool the carrier of L);
coherence
 for b1 being Subset of L st b1 is empty holds
( b1 is initial & b1 is final )
proof
let S be Subset of L; ::_thesis: ( S is empty implies ( S is initial & S is final ) )
assume A1: S is empty ; ::_thesis: ( S is initial & S is final )
thus  S is initial ::_thesis: S is final
proof
let p be Element of L; :: according to LATTICES:def_22 ::_thesis: for q being Element of L st p [= q & q in S holds
p in S
thus  for q being Element of L st p [= q & q in S holds
p in S by A1; ::_thesis: verum
end;
let p be Element of L; :: according to LATTICES:def_23 ::_thesis: for q being Element of L st p [= q & p in S holds
q in S
thus  for q being Element of L st p [= q & p in S holds
q in S by A1; ::_thesis: verum
end;
cluster initial  ->  meet-closed for M2( bool the carrier of L);
coherence
 for b1 being Subset of L st b1 is initial holds
b1 is meet-closed
proof
let S be Subset of L; ::_thesis: ( S is initial implies S is meet-closed )
assume A2: S is initial ; ::_thesis: S is meet-closed
let p, q be Element of L; :: according to LATTICES:def_24 ::_thesis: ( p in S & q in S implies p "/\" q in S )
assume that
 p in S and
A3: q in S ; ::_thesis: p "/\" q in S
thus  p "/\" q in S by A2, A3, Def22, Th6; ::_thesis: verum
end;
cluster final  ->  join-closed for M2( bool the carrier of L);
coherence
 for b1 being Subset of L st b1 is final holds
b1 is join-closed
proof
let S be Subset of L; ::_thesis: ( S is final implies S is join-closed )
assume A4: S is final ; ::_thesis: S is join-closed
let p, q be Element of L; :: according to LATTICES:def_25 ::_thesis: ( p in S & q in S implies p "\/" q in S )
assume that
 p in S and
A5: q in S ; ::_thesis: p "\/" q in S
thus  p "\/" q in S by A4, A5, Def23, Th5; ::_thesis: verum
end;
end;

theorem :: LATTICES:27
for L being Lattice
for S being non empty initial final Subset of L holds S = [#] L
proof
let L be Lattice; ::_thesis: for S being non empty initial final Subset of L holds S = [#] L
let S be non empty initial final Subset of L; ::_thesis: S = [#] 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; ::_thesis: ( x in S iff x in [#] L )
thus  ( x in S implies x in [#] L ) ; ::_thesis: ( x in [#] L implies x in S )
assume  x in [#] L ; ::_thesis: x in S
A2: x "/\" p in S by A1, Def22, Th6;
thus  x in S by A2, Def23, Th6; ::_thesis: verum
end;
hence  S = [#] L by SUBSET_1:3; ::_thesis: verum
end;