:: LATTICE3 semantic presentation

deffunc H1( LattStr ) -> set = the carrier of a1;

deffunc H2( LattStr ) -> Relation of [:the carrier of a1,the carrier of a1:],the carrier of a1 = the L_join of a1;

deffunc H3( LattStr ) -> Relation of [:the carrier of a1,the carrier of a1:],the carrier of a1 = the L_meet of a1;

definition
let c1 be set ;
func BooleLatt c1 -> strict LattStr means :Def1: :: LATTICE3:def 1
( the carrier of a2 = bool a1 & ( for b1, b2 being Subset of a1 holds
( the L_join of a2 . b1,b2 = b1 \/ b2 & the L_meet of a2 . b1,b2 = b1 /\ b2 ) ) );
existence
ex b1 being strict LattStr st
( the carrier of b1 = bool c1 & ( for b2, b3 being Subset of c1 holds
( the L_join of b1 . b2,b3 = b2 \/ b3 & the L_meet of b1 . b2,b3 = b2 /\ b3 ) ) )
proof end;
uniqueness
for b1, b2 being strict LattStr st the carrier of b1 = bool c1 & ( for b3, b4 being Subset of c1 holds
( the L_join of b1 . b3,b4 = b3 \/ b4 & the L_meet of b1 . b3,b4 = b3 /\ b4 ) ) & the carrier of b2 = bool c1 & ( for b3, b4 being Subset of c1 holds
( the L_join of b2 . b3,b4 = b3 \/ b4 & the L_meet of b2 . b3,b4 = b3 /\ b4 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines BooleLatt LATTICE3:def 1 :
for b1 being set
for b2 being strict LattStr holds
( b2 = BooleLatt b1 iff ( the carrier of b2 = bool b1 & ( for b3, b4 being Subset of b1 holds
( the L_join of b2 . b3,b4 = b3 \/ b4 & the L_meet of b2 . b3,b4 = b3 /\ b4 ) ) ) );

registration
let c1 be set ;
cluster BooleLatt a1 -> non empty strict ;
coherence
not BooleLatt c1 is empty
proof end;
end;

theorem Th1: :: LATTICE3:1
for b1 being set
for b2, b3 being Element of (BooleLatt b1) holds
( b2 "\/" b3 = b2 \/ b3 & b2 "/\" b3 = b2 /\ b3 )
proof end;

theorem Th2: :: LATTICE3:2
for b1 being set
for b2, b3 being Element of (BooleLatt b1) holds
( b2 [= b3 iff b2 c= b3 )
proof end;

registration
let c1 be set ;
cluster BooleLatt a1 -> non empty strict Lattice-like ;
coherence
BooleLatt c1 is Lattice-like
proof end;
end;

theorem Th3: :: LATTICE3:3
for b1 being set holds
( BooleLatt b1 is lower-bounded & Bottom (BooleLatt b1) = {} )
proof end;

theorem Th4: :: LATTICE3:4
for b1 being set holds
( BooleLatt b1 is upper-bounded & Top (BooleLatt b1) = b1 )
proof end;

registration
let c1 be set ;
cluster BooleLatt a1 -> non empty strict Lattice-like Boolean ;
coherence
( BooleLatt c1 is Boolean & BooleLatt c1 is Lattice-like )
proof end;
end;

theorem Th5: :: LATTICE3:5
for b1 being set
for b2 being Element of (BooleLatt b1) holds b2 ` = b1 \ b2
proof end;

definition
let c1 be Lattice;
redefine func LattRel as LattRel c1 -> Order of the carrier of a1;
coherence
LattRel c1 is Order of the carrier of c1
proof end;
end;

definition
let c1 be Lattice;
func LattPOSet c1 -> strict Poset equals :: LATTICE3:def 2
 RelStr(# the carrier of a1,(LattRel a1) #);
correctness
coherence
RelStr(# the carrier of c1,(LattRel c1) #) is strict Poset;
;
end;

:: deftheorem Def2 defines LattPOSet LATTICE3:def 2 :
for b1 being Lattice holds LattPOSet b1 = RelStr(# the carrier of b1,(LattRel b1) #);

registration
let c1 be Lattice;
cluster LattPOSet a1 -> non empty strict ;
coherence
not LattPOSet c1 is empty ;
end;

theorem Th6: :: LATTICE3:6
for b1, b2 being Lattice st LattPOSet b1 = LattPOSet b2 holds
LattStr(# the carrier of b1,the L_join of b1,the L_meet of b1 #) = LattStr(# the carrier of b2,the L_join of b2,the L_meet of b2 #)
proof end;

definition
let c1 be Lattice;
let c2 be Element of c1;
func c2 % -> Element of (LattPOSet a1) equals :: LATTICE3:def 3
a2;
correctness
coherence
c2 is Element of (LattPOSet c1);
;
end;

:: deftheorem Def3 defines % LATTICE3:def 3 :
for b1 being Lattice
for b2 being Element of b1 holds b2 % = b2;

definition
let c1 be Lattice;
let c2 be Element of (LattPOSet c1);
func % c2 -> Element of a1 equals :: LATTICE3:def 4
a2;
correctness
coherence
c2 is Element of c1;
;
end;

:: deftheorem Def4 defines % LATTICE3:def 4 :
for b1 being Lattice
for b2 being Element of (LattPOSet b1) holds % b2 = b2;

theorem Th7: :: LATTICE3:7
for b1 being Lattice
for b2, b3 being Element of b1 holds
( b2 [= b3 iff b2 % <= b3 % )
proof end;

definition
let c1 be set ;
let c2 be Order of c1;
redefine func ~ as c2 ~ -> Order of a1;
coherence
c2 ~ is Order of c1
proof end;
end;

definition
let c1 be RelStr ;
func c1 ~ -> strict RelStr equals :: LATTICE3:def 5
 RelStr(# the carrier of a1,(the InternalRel of a1 ~ ) #);
correctness
coherence
RelStr(# the carrier of c1,(the InternalRel of c1 ~ ) #) is strict RelStr ;
;
end;

:: deftheorem Def5 defines ~ LATTICE3:def 5 :
for b1 being RelStr holds b1 ~ = RelStr(# the carrier of b1,(the InternalRel of b1 ~ ) #);

registration
let c1 be Poset;
cluster a1 ~ -> strict reflexive transitive antisymmetric ;
coherence
( c1 ~ is reflexive & c1 ~ is transitive & c1 ~ is antisymmetric )
proof end;
end;

registration
let c1 be non empty RelStr ;
cluster a1 ~ -> non empty strict ;
coherence
not c1 ~ is empty ;
end;

theorem Th8: :: LATTICE3:8
for b1 being RelStr holds (b1 ~ ) ~ = RelStr(# the carrier of b1,the InternalRel of b1 #) ;

definition
let c1 be RelStr ;
let c2 be Element of c1;
func c2 ~ -> Element of (a1 ~ ) equals :: LATTICE3:def 6
a2;
correctness
coherence
c2 is Element of (c1 ~ );
;
end;

:: deftheorem Def6 defines ~ LATTICE3:def 6 :
for b1 being RelStr
for b2 being Element of b1 holds b2 ~ = b2;

definition
let c1 be RelStr ;
let c2 be Element of (c1 ~ );
func ~ c2 -> Element of a1 equals :: LATTICE3:def 7
a2;
correctness
coherence
c2 is Element of c1;
;
end;

:: deftheorem Def7 defines ~ LATTICE3:def 7 :
for b1 being RelStr
for b2 being Element of (b1 ~ ) holds ~ b2 = b2;

theorem Th9: :: LATTICE3:9
for b1 being RelStr
for b2, b3 being Element of b1 holds
( b2 <= b3 iff b3 ~ <= b2 ~ )
proof end;

definition
let c1 be RelStr ;
let c2 be set ;
let c3 be Element of c1;
pred c3 is_<=_than c2 means :: LATTICE3:def 8
for b1 being Element of a1 st b1 in a2 holds
a3 <= b1;
pred c2 is_<=_than c3 means :Def9: :: LATTICE3:def 9
for b1 being Element of a1 st b1 in a2 holds
b1 <= a3;
end;

:: deftheorem Def8 defines is_<=_than LATTICE3:def 8 :
for b1 being RelStr
for b2 being set
for b3 being Element of b1 holds
( b3 is_<=_than b2 iff for b4 being Element of b1 st b4 in b2 holds
b3 <= b4 );

:: deftheorem Def9 defines is_<=_than LATTICE3:def 9 :
for b1 being RelStr
for b2 being set
for b3 being Element of b1 holds
( b2 is_<=_than b3 iff for b4 being Element of b1 st b4 in b2 holds
b4 <= b3 );

notation
let c1 be RelStr ;
let c2 be set ;
let c3 be Element of c1;
synonym c2 is_>=_than c3 for c3 is_<=_than c2;
synonym c3 is_>=_than c2 for c2 is_<=_than c3;
end;

definition
let c1 be RelStr ;
attr a1 is with_suprema means :Def10: :: LATTICE3:def 10
for b1, b2 being Element of a1 ex b3 being Element of a1 st
( b1 <= b3 & b2 <= b3 & ( for b4 being Element of a1 st b1 <= b4 & b2 <= b4 holds
b3 <= b4 ) );
attr a1 is with_infima means :Def11: :: LATTICE3:def 11
for b1, b2 being Element of a1 ex b3 being Element of a1 st
( b3 <= b1 & b3 <= b2 & ( for b4 being Element of a1 st b4 <= b1 & b4 <= b2 holds
b4 <= b3 ) );
end;

:: deftheorem Def10 defines with_suprema LATTICE3:def 10 :
for b1 being RelStr holds
( b1 is with_suprema iff for b2, b3 being Element of b1 ex b4 being Element of b1 st
( b2 <= b4 & b3 <= b4 & ( for b5 being Element of b1 st b2 <= b5 & b3 <= b5 holds
b4 <= b5 ) ) );

:: deftheorem Def11 defines with_infima LATTICE3:def 11 :
for b1 being RelStr holds
( b1 is with_infima iff for b2, b3 being Element of b1 ex b4 being Element of b1 st
( b4 <= b2 & b4 <= b3 & ( for b5 being Element of b1 st b5 <= b2 & b5 <= b3 holds
b5 <= b4 ) ) );

registration
cluster with_suprema -> non empty RelStr ;
coherence
for b1 being RelStr st b1 is with_suprema holds
not b1 is empty
proof end;
cluster with_infima -> non empty RelStr ;
coherence
for b1 being RelStr st b1 is with_infima holds
not b1 is empty
proof end;
end;

theorem Th10: :: LATTICE3:10
for b1 being RelStr holds
( b1 is with_suprema iff b1 ~ is with_infima )
proof end;

theorem Th11: :: LATTICE3:11
for b1 being Lattice holds
( LattPOSet b1 is with_suprema & LattPOSet b1 is with_infima )
proof end;

definition
let c1 be RelStr ;
attr a1 is complete means :Def12: :: LATTICE3:def 12
for b1 being set ex b2 being Element of a1 st
( b1 is_<=_than b2 & ( for b3 being Element of a1 st b1 is_<=_than b3 holds
b2 <= b3 ) );
end;

:: deftheorem Def12 defines complete LATTICE3:def 12 :
for b1 being RelStr holds
( b1 is complete iff for b2 being set ex b3 being Element of b1 st
( b2 is_<=_than b3 & ( for b4 being Element of b1 st b2 is_<=_than b4 holds
b3 <= b4 ) ) );

registration
cluster non empty strict complete RelStr ;
existence
ex b1 being Poset st
( b1 is strict & b1 is complete & not b1 is empty )
proof end;
end;

theorem Th12: :: LATTICE3:12
for b1 being non empty RelStr st b1 is complete holds
( b1 is with_suprema & b1 is with_infima )
proof end;

registration
cluster non empty strict with_suprema with_infima complete RelStr ;
existence
ex b1 being Poset st
( b1 is complete & b1 is with_suprema & b1 is with_infima & b1 is strict & not b1 is empty )
proof end;
end;

definition
let c1 be RelStr ;
assume E14: c1 is antisymmetric ;
let c2, c3 be Element of c1;
assume E15: ex b1 being Element of c1 st
( c2 <= b1 & c3 <= b1 & ( for b2 being Element of c1 st c2 <= b2 & c3 <= b2 holds
b1 <= b2 ) ) ;
func c2 "\/" c3 -> Element of a1 means :Def13: :: LATTICE3:def 13
( a2 <= a4 & a3 <= a4 & ( for b1 being Element of a1 st a2 <= b1 & a3 <= b1 holds
a4 <= b1 ) );
existence
ex b1 being Element of c1 st
( c2 <= b1 & c3 <= b1 & ( for b2 being Element of c1 st c2 <= b2 & c3 <= b2 holds
b1 <= b2 ) ) by E15;
uniqueness
for b1, b2 being Element of c1 st c2 <= b1 & c3 <= b1 & ( for b3 being Element of c1 st c2 <= b3 & c3 <= b3 holds
b1 <= b3 ) & c2 <= b2 & c3 <= b2 & ( for b3 being Element of c1 st c2 <= b3 & c3 <= b3 holds
b2 <= b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines "\/" LATTICE3:def 13 :
for b1 being RelStr st b1 is antisymmetric holds
for b2, b3 being Element of b1 st ex b4 being Element of b1 st
( b2 <= b4 & b3 <= b4 & ( for b5 being Element of b1 st b2 <= b5 & b3 <= b5 holds
b4 <= b5 ) ) holds
for b4 being Element of b1 holds
( b4 = b2 "\/" b3 iff ( b2 <= b4 & b3 <= b4 & ( for b5 being Element of b1 st b2 <= b5 & b3 <= b5 holds
b4 <= b5 ) ) );

E15: now
let c1 be non empty antisymmetric with_suprema RelStr ;
let c2, c3 be Element of c1;
ex b1 being Element of c1 st
( c2 <= b1 & c3 <= b1 & ( for b2 being Element of c1 st c2 <= b2 & c3 <= b2 holds
b1 <= b2 ) ) by Def10;
hence for b1 being Element of c1 holds
( b1 = c2 "\/" c3 iff ( c2 <= b1 & c3 <= b1 & ( for b2 being Element of c1 st c2 <= b2 & c3 <= b2 holds
b1 <= b2 ) ) ) by Def13;
end;

definition
let c1 be RelStr ;
assume E16: c1 is antisymmetric ;
let c2, c3 be Element of c1;
assume E17: ex b1 being Element of c1 st
( c2 >= b1 & c3 >= b1 & ( for b2 being Element of c1 st c2 >= b2 & c3 >= b2 holds
b1 >= b2 ) ) ;
func c2 "/\" c3 -> Element of a1 means :Def14: :: LATTICE3:def 14
( a4 <= a2 & a4 <= a3 & ( for b1 being Element of a1 st b1 <= a2 & b1 <= a3 holds
b1 <= a4 ) );
existence
ex b1 being Element of c1 st
( b1 <= c2 & b1 <= c3 & ( for b2 being Element of c1 st b2 <= c2 & b2 <= c3 holds
b2 <= b1 ) ) by E17;
uniqueness
for b1, b2 being Element of c1 st b1 <= c2 & b1 <= c3 & ( for b3 being Element of c1 st b3 <= c2 & b3 <= c3 holds
b3 <= b1 ) & b2 <= c2 & b2 <= c3 & ( for b3 being Element of c1 st b3 <= c2 & b3 <= c3 holds
b3 <= b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines "/\" LATTICE3:def 14 :
for b1 being RelStr st b1 is antisymmetric holds
for b2, b3 being Element of b1 st ex b4 being Element of b1 st
( b2 >= b4 & b3 >= b4 & ( for b5 being Element of b1 st b2 >= b5 & b3 >= b5 holds
b4 >= b5 ) ) holds
for b4 being Element of b1 holds
( b4 = b2 "/\" b3 iff ( b4 <= b2 & b4 <= b3 & ( for b5 being Element of b1 st b5 <= b2 & b5 <= b3 holds
b5 <= b4 ) ) );

E17: now
let c1 be non empty antisymmetric with_infima RelStr ;
let c2, c3 be Element of c1;
ex b1 being Element of c1 st
( c2 >= b1 & c3 >= b1 & ( for b2 being Element of c1 st c2 >= b2 & c3 >= b2 holds
b1 >= b2 ) ) by Def11;
hence for b1 being Element of c1 holds
( b1 = c2 "/\" c3 iff ( c2 >= b1 & c3 >= b1 & ( for b2 being Element of c1 st c2 >= b2 & c3 >= b2 holds
b1 >= b2 ) ) ) by Def14;
end;

theorem Th13: :: LATTICE3:13
for b1 being antisymmetric with_suprema RelStr
for b2, b3 being Element of b1 holds b2 "\/" b3 = b3 "\/" b2
proof end;

theorem Th14: :: LATTICE3:14
for b1 being antisymmetric with_suprema RelStr
for b2, b3, b4 being Element of b1 st b1 is transitive holds
(b2 "\/" b3) "\/" b4 = b2 "\/" (b3 "\/" b4)
proof end;

theorem Th15: :: LATTICE3:15
for b1 being antisymmetric with_infima RelStr
for b2, b3 being Element of b1 holds b2 "/\" b3 = b3 "/\" b2
proof end;

theorem Th16: :: LATTICE3:16
for b1 being antisymmetric with_infima RelStr
for b2, b3, b4 being Element of b1 st b1 is transitive holds
(b2 "/\" b3) "/\" b4 = b2 "/\" (b3 "/\" b4)
proof end;

definition
let c1 be antisymmetric with_infima RelStr ;
let c2, c3 be Element of c1;
redefine func "/\" as c2 "/\" c3 -> Element of a1;
commutativity
for b1, b2 being Element of c1 holds b1 "/\" b2 = b2 "/\" b1 by Th15;
end;

definition
let c1 be antisymmetric with_suprema RelStr ;
let c2, c3 be Element of c1;
redefine func "\/" as c2 "\/" c3 -> Element of a1;
commutativity
for b1, b2 being Element of c1 holds b1 "\/" b2 = b2 "\/" b1 by Th13;
end;

theorem Th17: :: LATTICE3:17
for b1 being reflexive antisymmetric with_suprema with_infima RelStr
for b2, b3 being Element of b1 holds (b2 "/\" b3) "\/" b3 = b3
proof end;

theorem Th18: :: LATTICE3:18
for b1 being reflexive antisymmetric with_suprema with_infima RelStr
for b2, b3 being Element of b1 holds b2 "/\" (b2 "\/" b3) = b2
proof end;

theorem Th19: :: LATTICE3:19
for b1 being with_suprema with_infima Poset ex b2 being strict Lattice st RelStr(# the carrier of b1,the InternalRel of b1 #) = LattPOSet b2
proof end;

definition
let c1 be RelStr ;
assume E25: c1 is with_suprema with_infima Poset ;
func latt c1 -> strict Lattice means :Def15: :: LATTICE3:def 15
 RelStr(# the carrier of a1,the InternalRel of a1 #) = LattPOSet a2;
existence
ex b1 being strict Lattice st RelStr(# the carrier of c1,the InternalRel of c1 #) = LattPOSet b1 by E25, Th19;
uniqueness
for b1, b2 being strict Lattice st RelStr(# the carrier of c1,the InternalRel of c1 #) = LattPOSet b1 & RelStr(# the carrier of c1,the InternalRel of c1 #) = LattPOSet b2 holds
b1 = b2 by Th6;
end;

:: deftheorem Def15 defines latt LATTICE3:def 15 :
for b1 being RelStr st b1 is with_suprema with_infima Poset holds
for b2 being strict Lattice holds
( b2 = latt b1 iff RelStr(# the carrier of b1,the InternalRel of b1 #) = LattPOSet b2 );

theorem Th20: :: LATTICE3:20
for b1 being Lattice holds
( (LattRel b1) ~ = LattRel (b1 .: ) & (LattPOSet b1) ~ = LattPOSet (b1 .: ) )
proof end;

definition
let c1 be non empty LattStr ;
let c2 be Element of c1;
let c3 be set ;
pred c2 is_less_than c3 means :Def16: :: LATTICE3:def 16
for b1 being Element of a1 st b1 in a3 holds
a2 [= b1;
pred c3 is_less_than c2 means :Def17: :: LATTICE3:def 17
for b1 being Element of a1 st b1 in a3 holds
b1 [= a2;
end;

:: deftheorem Def16 defines is_less_than LATTICE3:def 16 :
for b1 being non empty LattStr
for b2 being Element of b1
for b3 being set holds
( b2 is_less_than b3 iff for b4 being Element of b1 st b4 in b3 holds
b2 [= b4 );

:: deftheorem Def17 defines is_less_than LATTICE3:def 17 :
for b1 being non empty LattStr
for b2 being Element of b1
for b3 being set holds
( b3 is_less_than b2 iff for b4 being Element of b1 st b4 in b3 holds
b4 [= b2 );

notation
let c1 be non empty LattStr ;
let c2 be Element of c1;
let c3 be set ;
synonym c3 is_great_than c2 for c2 is_less_than c3;
synonym c2 is_great_than c3 for c3 is_less_than c2;
end;

theorem Th21: :: LATTICE3:21
for b1 being Lattice
for b2, b3, b4 being Element of b1 holds
( b2 is_less_than {b3,b4} iff b2 [= b3 "/\" b4 )
proof end;

theorem Th22: :: LATTICE3:22
for b1 being Lattice
for b2, b3, b4 being Element of b1 holds
( b2 is_great_than {b3,b4} iff b3 "\/" b4 [= b2 )
proof end;

definition
let c1 be non empty LattStr ;
attr a1 is complete means :Def18: :: LATTICE3:def 18
for b1 being set ex b2 being Element of a1 st
( b1 is_less_than b2 & ( for b3 being Element of a1 st b1 is_less_than b3 holds
b2 [= b3 ) );
attr a1 is \/-distributive means :Def19: :: LATTICE3:def 19
for b1 being set
for b2, b3, b4 being Element of a1 st b1 is_less_than b2 & ( for b5 being Element of a1 st b1 is_less_than b5 holds
b2 [= b5 ) & { (b3 "/\" b5) where B is Element of a1 : b5 in b1 } is_less_than b4 & ( for b5 being Element of a1 st { (b3 "/\" b6) where B is Element of a1 : b6 in b1 } is_less_than b5 holds
b4 [= b5 ) holds
b3 "/\" b2 [= b4;
attr a1 is /\-distributive means :: LATTICE3:def 20
for b1 being set
for b2, b3, b4 being Element of a1 st b1 is_great_than b2 & ( for b5 being Element of a1 st b1 is_great_than b5 holds
b5 [= b2 ) & { (b3 "\/" b5) where B is Element of a1 : b5 in b1 } is_great_than b4 & ( for b5 being Element of a1 st { (b3 "\/" b6) where B is Element of a1 : b6 in b1 } is_great_than b5 holds
b5 [= b4 ) holds
b4 [= b3 "\/" b2;
end;

:: deftheorem Def18 defines complete LATTICE3:def 18 :
for b1 being non empty LattStr holds
( b1 is complete iff for b2 being set ex b3 being Element of b1 st
( b2 is_less_than b3 & ( for b4 being Element of b1 st b2 is_less_than b4 holds
b3 [= b4 ) ) );

:: deftheorem Def19 defines \/-distributive LATTICE3:def 19 :
for b1 being non empty LattStr holds
( b1 is \/-distributive iff for b2 being set
for b3, b4, b5 being Element of b1 st b2 is_less_than b3 & ( for b6 being Element of b1 st b2 is_less_than b6 holds
b3 [= b6 ) & { (b4 "/\" b6) where B is Element of b1 : b6 in b2 } is_less_than b5 & ( for b6 being Element of b1 st { (b4 "/\" b7) where B is Element of b1 : b7 in b2 } is_less_than b6 holds
b5 [= b6 ) holds
b4 "/\" b3 [= b5 );

:: deftheorem Def20 defines /\-distributive LATTICE3:def 20 :
for b1 being non empty LattStr holds
( b1 is /\-distributive iff for b2 being set
for b3, b4, b5 being Element of b1 st b2 is_great_than b3 & ( for b6 being Element of b1 st b2 is_great_than b6 holds
b6 [= b3 ) & { (b4 "\/" b6) where B is Element of b1 : b6 in b2 } is_great_than b5 & ( for b6 being Element of b1 st { (b4 "\/" b7) where B is Element of b1 : b7 in b2 } is_great_than b6 holds
b6 [= b5 ) holds
b5 [= b4 "\/" b3 );

theorem Th23: :: LATTICE3:23
for b1 being set
for b2 being B_Lattice
for b3 being Element of b2 holds
( b1 is_less_than b3 iff { (b4 ` ) where B is Element of b2 : b4 in b1 } is_great_than b3 ` )
proof end;

theorem Th24: :: LATTICE3:24
for b1 being set
for b2 being B_Lattice
for b3 being Element of b2 holds
( b1 is_great_than b3 iff { (b4 ` ) where B is Element of b2 : b4 in b1 } is_less_than b3 ` )
proof end;

theorem Th25: :: LATTICE3:25
for b1 being set holds BooleLatt b1 is complete
proof end;

theorem Th26: :: LATTICE3:26
for b1 being set holds BooleLatt b1 is \/-distributive
proof end;

theorem Th27: :: LATTICE3:27
for b1 being set holds BooleLatt b1 is /\-distributive
proof end;

registration
cluster strict complete \/-distributive /\-distributive LattStr ;
existence
ex b1 being Lattice st
( b1 is complete & b1 is \/-distributive & b1 is /\-distributive & b1 is strict )
proof end;
end;

theorem Th28: :: LATTICE3:28
for b1 being set
for b2 being Lattice
for b3 being Element of b2 holds
( b3 is_less_than b1 iff b3 % is_<=_than b1 )
proof end;

theorem Th29: :: LATTICE3:29
for b1 being set
for b2 being Lattice
for b3 being Element of (LattPOSet b2) holds
( b3 is_<=_than b1 iff % b3 is_less_than b1 )
proof end;

theorem Th30: :: LATTICE3:30
for b1 being set
for b2 being Lattice
for b3 being Element of b2 holds
( b1 is_less_than b3 iff b1 is_<=_than b3 % )
proof end;

theorem Th31: :: LATTICE3:31
for b1 being set
for b2 being Lattice
for b3 being Element of (LattPOSet b2) holds
( b1 is_<=_than b3 iff b1 is_less_than % b3 )
proof end;

registration
let c1 be non empty complete Poset;
cluster latt a1 -> strict complete ;
coherence
latt c1 is complete
proof end;
end;

definition
let c1 be non empty LattStr ;
assume E37: c1 is complete Lattice ;
let c2 be set ;
func "\/" c2,c1 -> Element of a1 means :Def21: :: LATTICE3:def 21
( a2 is_less_than a3 & ( for b1 being Element of a1 st a2 is_less_than b1 holds
a3 [= b1 ) );
existence
ex b1 being Element of c1 st
( c2 is_less_than b1 & ( for b2 being Element of c1 st c2 is_less_than b2 holds
b1 [= b2 ) ) by E37, Def18;
uniqueness
for b1, b2 being Element of c1 st c2 is_less_than b1 & ( for b3 being Element of c1 st c2 is_less_than b3 holds
b1 [= b3 ) & c2 is_less_than b2 & ( for b3 being Element of c1 st c2 is_less_than b3 holds
b2 [= b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines "\/" LATTICE3:def 21 :
for b1 being non empty LattStr st b1 is complete Lattice holds
for b2 being set
for b3 being Element of b1 holds
( b3 = "\/" b2,b1 iff ( b2 is_less_than b3 & ( for b4 being Element of b1 st b2 is_less_than b4 holds
b3 [= b4 ) ) );

definition
let c1 be non empty LattStr ;
let c2 be set ;
func "/\" c2,c1 -> Element of a1 equals :: LATTICE3:def 22
 "\/" { b1 where B is Element of a1 : b1 is_less_than a2 } ,a1;
correctness
coherence
"\/" { b1 where B is Element of c1 : b1 is_less_than c2 } ,c1 is Element of c1;
;
end;

:: deftheorem Def22 defines "/\" LATTICE3:def 22 :
for b1 being non empty LattStr
for b2 being set holds "/\" b2,b1 = "\/" { b3 where B is Element of b1 : b3 is_less_than b2 } ,b1;

notation
let c1 be non empty LattStr ;
let c2 be Subset of c1;
synonym "\/" c2 for "\/" c2,c1;
synonym "/\" c2 for "/\" c2,c1;
end;

theorem Th32: :: LATTICE3:32
for b1 being complete Lattice
for b2 being Element of b1
for b3 being set holds "\/" { (b2 "/\" b4) where B is Element of b1 : b4 in b3 } ,b1 [= b2 "/\" ("\/" b3,b1)
proof end;

theorem Th33: :: LATTICE3:33
for b1 being complete Lattice holds
( b1 is \/-distributive iff for b2 being set
for b3 being Element of b1 holds b3 "/\" ("\/" b2,b1) [= "\/" { (b3 "/\" b4) where B is Element of b1 : b4 in b2 } ,b1 )
proof end;

theorem Th34: :: LATTICE3:34
for b1 being complete Lattice
for b2 being Element of b1
for b3 being set holds
( b2 = "/\" b3,b1 iff ( b2 is_less_than b3 & ( for b4 being Element of b1 st b4 is_less_than b3 holds
b4 [= b2 ) ) )
proof end;

theorem Th35: :: LATTICE3:35
for b1 being complete Lattice
for b2 being Element of b1
for b3 being set holds b2 "\/" ("/\" b3,b1) [= "/\" { (b2 "\/" b4) where B is Element of b1 : b4 in b3 } ,b1
proof end;

theorem Th36: :: LATTICE3:36
for b1 being complete Lattice holds
( b1 is /\-distributive iff for b2 being set
for b3 being Element of b1 holds "/\" { (b3 "\/" b4) where B is Element of b1 : b4 in b2 } ,b1 [= b3 "\/" ("/\" b2,b1) )
proof end;

theorem Th37: :: LATTICE3:37
for b1 being complete Lattice
for b2 being set holds "\/" b2,b1 = "/\" { b3 where B is Element of b1 : b3 is_great_than b2 } ,b1
proof end;

theorem Th38: :: LATTICE3:38
for b1 being complete Lattice
for b2 being Element of b1
for b3 being set st b2 in b3 holds
( b2 [= "\/" b3,b1 & "/\" b3,b1 [= b2 )
proof end;

theorem Th39: :: LATTICE3:39
canceled;

theorem Th40: :: LATTICE3:40
for b1 being complete Lattice
for b2 being Element of b1
for b3 being set st b2 is_less_than b3 holds
b2 [= "/\" b3,b1
proof end;

theorem Th41: :: LATTICE3:41
for b1 being complete Lattice
for b2 being Element of b1
for b3 being set st b2 in b3 & b3 is_less_than b2 holds
"\/" b3,b1 = b2
proof end;

theorem Th42: :: LATTICE3:42
for b1 being complete Lattice
for b2 being Element of b1
for b3 being set st b2 in b3 & b2 is_less_than b3 holds
"/\" b3,b1 = b2
proof end;

theorem Th43: :: LATTICE3:43
for b1 being complete Lattice
for b2 being Element of b1 holds
( "\/" {b2} = b2 & "/\" {b2} = b2 )
proof end;

theorem Th44: :: LATTICE3:44
for b1 being complete Lattice
for b2, b3 being Element of b1 holds
( b2 "\/" b3 = "\/" {b2,b3} & b2 "/\" b3 = "/\" {b2,b3} )
proof end;

theorem Th45: :: LATTICE3:45
for b1 being complete Lattice
for b2 being Element of b1 holds
( b2 = "\/" { b3 where B is Element of b1 : b3 [= b2 } ,b1 & b2 = "/\" { b3 where B is Element of b1 : b2 [= b3 } ,b1 )
proof end;

theorem Th46: :: LATTICE3:46
for b1 being complete Lattice
for b2, b3 being set st b2 c= b3 holds
( "\/" b2,b1 [= "\/" b3,b1 & "/\" b3,b1 [= "/\" b2,b1 )
proof end;

theorem Th47: :: LATTICE3:47
for b1 being complete Lattice
for b2 being set holds
( "\/" b2,b1 = "\/" { b3 where B is Element of b1 : ex b1 being Element of b1 st
( b3 [= b4 & b4 in b2 ) } ,b1 & "/\" b2,b1 = "/\" { b3 where B is Element of b1 : ex b1 being Element of b1 st
( b4 [= b3 & b4 in b2 ) } ,b1 )
proof end;

theorem Th48: :: LATTICE3:48
for b1 being complete Lattice
for b2, b3 being set st ( for b4 being Element of b1 st b4 in b2 holds
ex b5 being Element of b1 st
( b4 [= b5 & b5 in b3 ) ) holds
"\/" b2,b1 [= "\/" b3,b1
proof end;

theorem Th49: :: LATTICE3:49
for b1 being complete Lattice
for b2 being set st b2 c= bool the carrier of b1 holds
"\/" (union b2),b1 = "\/" { ("\/" b3) where B is Subset of b1 : b3 in b2 } ,b1
proof end;

theorem Th50: :: LATTICE3:50
for b1 being complete Lattice holds
( b1 is 0_Lattice & Bottom b1 = "\/" {} ,b1 )
proof end;

theorem Th51: :: LATTICE3:51
for b1 being complete Lattice holds
( b1 is 1_Lattice & Top b1 = "\/" the carrier of b1,b1 )
proof end;

theorem Th52: :: LATTICE3:52
for b1 being complete Lattice
for b2, b3 being Element of b1 st b1 is I_Lattice holds
b2 => b3 = "\/" { b4 where B is Element of b1 : b2 "/\" b4 [= b3 } ,b1
proof end;

theorem Th53: :: LATTICE3:53
for b1 being complete Lattice st b1 is I_Lattice holds
b1 is \/-distributive
proof end;

theorem Th54: :: LATTICE3:54
for b1 being set
for b2 being complete \/-distributive Lattice
for b3 being Element of b2 holds
( b3 "/\" ("\/" b1,b2) = "\/" { (b3 "/\" b4) where B is Element of b2 : b4 in b1 } ,b2 & ("\/" b1,b2) "/\" b3 = "\/" { (b4 "/\" b3) where B is Element of b2 : b4 in b1 } ,b2 )
proof end;

theorem Th55: :: LATTICE3:55
for b1 being set
for b2 being complete /\-distributive Lattice
for b3 being Element of b2 holds
( b3 "\/" ("/\" b1,b2) = "/\" { (b3 "\/" b4) where B is Element of b2 : b4 in b1 } ,b2 & ("/\" b1,b2) "\/" b3 = "/\" { (b4 "\/" b3) where B is Element of b2 : b4 in b1 } ,b2 )
proof end;

scheme :: LATTICE3:sch 1
s1{ F1() -> set , F2() -> non empty set , P1[ set ] } :
{ F1() where B is Element of F2() : P1[b1] } = {F1()}
provided
E50: ex b1 being Element of F2() st P1[b1]
proof end;

scheme :: LATTICE3:sch 2
s2{ F1() -> non empty set , F2() -> non empty set , F3( set ) -> Element of F2(), F4() -> Function, P1[ set ] } :
F4() .: { F3(b1) where B is Element of F1() : P1[b1] } = { (F4() . F3(b1)) where B is Element of F1() : P1[b1] }
provided
E50: F2() c= dom F4()
proof end;

E50: now
let c1 be non empty set ;
let c2 be Function of bool c1,c1;
assume that
E51: for b1 being Element of c1 holds c2 . {b1} = b1 and
E52: for b1 being Subset-Family of c1 holds c2 . (c2 .: b1) = c2 . (union b1) ;
defpred S1[ set , set ] means c2 . {a1,a2} = a2;
consider c3 being Relation of c1 such that
E53: for b1, b2 being set holds
( [b1,b2] in c3 iff ( b1 in c1 & b2 in c1 & S1[b1,b2] ) ) from RELSET_1:sch 1();
E54: dom c2 = bool c1 by FUNCT_2:def 1;
E55: now
let c4, c5 be Subset of c1;
thus c2 . {(c2 . c4),(c2 . c5)} = c2 . (c2 .: {c4,c5}) by E54, FUNCT_1:118
.= c2 . (union {c4,c5}) by E52
.= c2 . (c4 \/ c5) by ZFMISC_1:93 ;
end;
E56: for b1, b2 being Element of c1
for b3 being Subset of c1 st b2 in b3 holds
c2 . (b3 \/ {b1}) = c2 . { (c2 . {b4,b1}) where B is Element of c1 : b4 in b3 }
proof
let c4, c5 be Element of c1;
let c6 be Subset of c1;
assume E57: c5 in c6 ;
set c7 = { {b1,c4} where B is Element of c1 : b1 in c6 } ;
E58: c6 \/ {c4} = union { {b1,c4} where B is Element of c1 : b1 in c6 }
proof
thus c6 \/ {c4} c= union { {b1,c4} where B is Element of c1 : b1 in c6 } :: according to XBOOLE_0:def 10
proof
let c8 be set ; :: according to TARSKI:def 3
assume c8 in c6 \/ {c4} ;
then ( ( c8 in c6 & c6 c= c1 ) or c8 in {c4} ) by XBOOLE_0:def 2;
then ( ( c8 in c6 & c8 is Element of c1 ) or c8 = c4 ) by TARSKI:def 1;
then ( ( c8 in {c8,c4} & {c8,c4} in { {b1,c4} where B is Element of c1 : b1 in c6 } ) or ( c8 in {c5,c4} & {c5,c4} in { {b1,c4} where B is Element of c1 : b1 in c6 } ) ) by E57, TARSKI:def 2;
hence c8 in union { {b1,c4} where B is Element of c1 : b1 in c6 } by TARSKI:def 4;
end;
let c8 be set ; :: according to TARSKI:def 3
assume c8 in union { {b1,c4} where B is Element of c1 : b1 in c6 } ;
then consider c9 being set such that
E59: ( c8 in c9 & c9 in { {b1,c4} where B is Element of c1 : b1 in c6 } ) by TARSKI:def 4;
consider c10 being Element of c1 such that
E60: ( c9 = {c10,c4} & c10 in c6 ) by E59;
( c8 = c10 or ( c8 = c4 & c4 in {c4} ) ) by E59, E60, TARSKI:def 1, TARSKI:def 2;
hence c8 in c6 \/ {c4} by E60, XBOOLE_0:def 2;
end;
{ {b1,c4} where B is Element of c1 : b1 in c6 } c= bool c1
proof
let c8 be set ; :: according to TARSKI:def 3
assume c8 in { {b1,c4} where B is Element of c1 : b1 in c6 } ;
then ( c8 c= c6 \/ {c4} & c6 \/ {c4} c= c1 ) by E58, ZFMISC_1:92;
then c8 c= c1 by XBOOLE_1:1;
hence c8 in bool c1 ;
end;
then reconsider c8 = { {b1,c4} where B is Element of c1 : b1 in c6 } as Subset-Family of c1 ;
defpred S2[ set ] means a1 in c6;
deffunc H4( Element of c1) -> Element of bool c1 = {a1,c4};
E59: bool c1 c= dom c2 by FUNCT_2:def 1;
c2 .: { H4(b1) where B is Element of c1 : S2[b1] } = { (c2 . H4(b1)) where B is Element of c1 : S2[b1] } from LATTICE3:sch 2(E59);
 then c2 . (union c8) = c2 . { (c2 . {b1,c4}) where B is Element of c1 : b1 in c6 } by E52;
hence c2 . (c6 \/ {c4}) = c2 . { (c2 . {b1,c4}) where B is Element of c1 : b1 in c6 } by E58;
end;
E57: c3 is_reflexive_in c1
proof
let c4 be set ; :: according to RELAT_2:def 1
assume E58: c4 in c1 ;
then c4 = c2 . {c4} by E51
.= c2 . {c4,c4} by ENUMSET1:69 ;
hence [c4,c4] in c3 by E53, E58;
end;
E58: c3 is_antisymmetric_in c1
proof
let c4, c5 be set ; :: according to RELAT_2:def 4
assume ( c4 in c1 & c5 in c1 & [c4,c5] in c3 & [c5,c4] in c3 ) ;
then ( c2 . {c4,c5} = c5 & c2 . {c5,c4} = c4 ) by E53;
hence c4 = c5 ;
end;
E59: c3 is_transitive_in c1
proof
let c4, c5, c6 be set ; :: according to RELAT_2:def 8
assume E60: ( c4 in c1 & c5 in c1 & c6 in c1 & [c4,c5] in c3 & [c5,c6] in c3 ) ;
then reconsider c7 = c4, c8 = c5, c9 = c6 as Element of c1 ;
E61: ( c2 . {c4,c5} = c5 & c2 . {c5,c6} = c6 ) by E53, E60;
then c2 . {c7,c9} = c2 . {(c2 . {c7}),(c2 . {c8,c9})} by E51
.= c2 . ({c7} \/ {c8,c9}) by E55
.= c2 . {c7,c8,c9} by ENUMSET1:42
.= c2 . ({c7,c8} \/ {c9}) by ENUMSET1:43
.= c2 . {(c2 . {c7,c8}),(c2 . {c9})} by E55
.= c9 by E51, E61 ;
hence [c4,c6] in c3 by E53;
end;
E60: dom c3 = c1 by E57, ORDERS_1:98;
field c3 = c1 by E57, ORDERS_1:98;
then reconsider c4 = c3 as Order of c1 by E57, E58, E59, E60, PARTFUN1:def 4, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;
set c5 = RelStr(# c1,c4 #);
RelStr(# c1,c4 #) is complete
proof
let c6 be set ; :: according to LATTICE3:def 12
reconsider c7 = c6 /\ c1 as Subset of c1 by XBOOLE_1:17;
reconsider c8 = c2 . c7 as Element of RelStr(# c1,c4 #) ;
take c8 ;
thus c6 is_<=_than c8
proof
let c9 be Element of RelStr(# c1,c4 #); :: according to LATTICE3:def 9
assume c9 in c6 ;
then c9 in c7 by XBOOLE_0:def 3;
then {c9} \/ c7 = c7 by ZFMISC_1:46;
then c8 = c2 . {(c2 . {c9}),c8} by E55
.= c2 . {c9,c8} by E51 ;
hence [c9,c8] in the InternalRel of RelStr(# c1,c4 #) by E53; :: according to ORDERS_2:def 9
end;
let c9 be Element of RelStr(# c1,c4 #);
assume E61: c6 is_<=_than c9 ;
E62: c2 . {c8,c9} = c2 . {c8,(c2 . {c9})} by E51
.= c2 . (c7 \/ {c9}) by E55 ;
now
per cases ( c7 <> {} or c7 = {} ) ;
suppose E63: c7 <> {} ;
consider c10 being Element of c7;
reconsider c11 = c10 as Element of c1 by E63, TARSKI:def 3;
deffunc H4( Element of c1) -> set = c2 . {a1,c9};
deffunc H5( Element of c1) -> Element of RelStr(# c1,c4 #) = c9;
defpred S2[ set ] means a1 in c7;
E64: for b1 being Element of c1 st S2[b1] holds
H4(b1) = H5(b1)
proof
let c12 be Element of c1;
reconsider c13 = c12 as Element of RelStr(# c1,c4 #) ;
reconsider c14 = c9 as Element of c1 ;
assume c12 in c7 ;
then c12 in c6 by XBOOLE_0:def 3;
then c13 <= c9 by E61, Def9;
then [c12,c14] in c4 by ORDERS_2:def 9;
hence H4(c12) = H5(c12) by E53;
end;
E65: c11 in c7 by E63;
then E66: ex b1 being Element of c1 st S2[b1] ;
{ H4(b1) where B is Element of c1 : S2[b1] } = { H5(b1) where B is Element of c1 : S2[b1] } from FRAENKEL:sch 6(E64)
.= { c9 where B is Element of c1 : S2[b1] }
.= {c9} from LATTICE3:sch 1(E66) ;
hence c2 . {c8,c9} = c2 . {c9} by E56, E62, E65
.= c9 by E51 ;

end;
suppose c7 = {} ;
hence c2 . {c8,c9} = c9 by E51, E62;
end;
end;
end;
hence [c8,c9] in the InternalRel of RelStr(# c1,c4 #) by E53; :: according to ORDERS_2:def 9
end;
then reconsider c6 = RelStr(# c1,c4 #) as non empty strict complete Poset ;
take c7 = latt c6;
E61: ( c6 is with_suprema & c6 is with_infima ) by Th12;
then E62: ( c6 = LattPOSet c7 & LattPOSet c7 = RelStr(# H1(c7),(LattRel c7) #) ) by Def15;
hence H1(c7) = c1 ;
let c8 be Subset of c7;
reconsider c9 = c8 as Subset of c1 by E62;
reconsider c10 = c2 . c9 as Element of (LattPOSet c7) by E61, Def15;
set c11 = % c10;
c8 is_<=_than c10
proof
let c12 be Element of (LattPOSet c7); :: according to LATTICE3:def 9
reconsider c13 = c12 as Element of c1 by E61, Def15;
assume c12 in c8 ;
then E63: c8 = {c12} \/ c8 by ZFMISC_1:46;
c2 . {c13,(c2 . c9)} = c2 . {(c2 . {c13}),(c2 . c9)} by E51
.= c10 by E55, E63 ;
hence [c12,c10] in the InternalRel of (LattPOSet c7) by E53, E62; :: according to ORDERS_2:def 9
end;
then E63: c8 is_less_than % c10 by Th31;
now
let c12 be Element of c7;
reconsider c13 = c12 as Element of c1 by E62;
reconsider c14 = c13 as Element of (LattPOSet c7) ;
assume c8 is_less_than c12 ;
then E64: ( c8 is_<=_than c12 % & c14 = c12 % ) by Th30;
E65: c2 . {(c2 . c9),c14} = c2 . {(c2 . c9),(c2 . {c13})} by E51
.= c2 . (c9 \/ {c14}) by E55 ;
now
per cases ( c9 <> {} or c9 = {} ) ;
suppose E66: c9 <> {} ;
consider c15 being Element of c9;
reconsider c16 = c15 as Element of c1 by E66, TARSKI:def 3;
deffunc H4( Element of c1) -> set = c2 . {a1,c14};
deffunc H5( Element of c1) -> Element of (LattPOSet c7) = c14;
defpred S2[ set ] means a1 in c9;
E67: for b1 being Element of c1 st S2[b1] holds
H4(b1) = H5(b1)
proof
let c17 be Element of c1;
reconsider c18 = c17 as Element of (LattPOSet c7) by E61, Def15;
assume c17 in c9 ;
then c18 <= c14 by E64, Def9;
then [c17,c13] in c4 by E62, ORDERS_2:def 9;
hence H4(c17) = H5(c17) by E53;
end;
E68: c16 in c9 by E66;
then E69: ex b1 being Element of c1 st S2[b1] ;
{ H4(b1) where B is Element of c1 : S2[b1] } = { H5(b1) where B is Element of c1 : S2[b1] } from FRAENKEL:sch 6(E67)
.= { c14 where B is Element of c1 : S2[b1] }
.= {c14} from LATTICE3:sch 1(E69) ;
hence c2 . {c10,c14} = c2 . {c14} by E56, E65, E68
.= c14 by E51 ;

end;
suppose c9 = {} ;
hence c2 . {c10,c14} = c14 by E51, E65;
end;
end;
end;
then [c10,c14] in the InternalRel of (LattPOSet c7) by E53, E62;
then ( c10 <= c14 & (% c10) % = % c10 & c10 = % c10 & c12 % = c14 ) by ORDERS_2:def 9;
hence % c10 [= c12 by Th7;
end;
hence "\/" c8 = % c10 by E63, Def21
.= c2 . c8 ;

end;

theorem Th56: :: LATTICE3:56
for b1 being non empty set
for b2 being Function of bool b1,b1 st ( for b3 being Element of b1 holds b2 . {b3} = b3 ) & ( for b3 being Subset-Family of b1 holds b2 . (b2 .: b3) = b2 . (union b3) ) holds
ex b3 being strict complete Lattice st
( the carrier of b3 = b1 & ( for b4 being Subset of b3 holds "\/" b4 = b2 . b4 ) ) by Lemma50;