:: LATTICE3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

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

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

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

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

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

theorem Th1: :: LATTICE3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for x, y being Element of (BooleLatt X) holds
( x "\/" y = x \/ y & x "/\" y = x /\ y )
proof end;

theorem Th2: :: LATTICE3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for x, y being Element of (BooleLatt X) holds
( x [= y iff x c= y )
proof end;

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

theorem Th3: :: LATTICE3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds
( BooleLatt X is lower-bounded & Bottom (BooleLatt X) = {} )
proof end;

theorem Th4: :: LATTICE3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds
( BooleLatt X is upper-bounded & Top (BooleLatt X) = X )
proof end;

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

theorem :: LATTICE3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for x being Element of (BooleLatt X) holds x ` = X \ x
proof end;

definition
let L be Lattice;
:: original: LattRel
redefine func LattRel L -> Order of the carrier of L;
coherence
LattRel L is Order of the carrier of L
proof end;
end;

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

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

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

theorem Th6: :: LATTICE3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being Lattice st LattPOSet L1 = LattPOSet L2 holds
LattStr(# the carrier of L1,the L_join of L1,the L_meet of L1 #) = LattStr(# the carrier of L2,the L_join of L2,the L_meet of L2 #)
proof end;

definition
let L be Lattice;
let p be Element of L;
func p % -> Element of (LattPOSet L) equals :: LATTICE3:def 3
p;
correctness
coherence
p is Element of (LattPOSet L);
;
end;

:: deftheorem defines % LATTICE3:def 3 :
for L being Lattice
for p being Element of L holds p % = p;

definition
let L be Lattice;
let p be Element of (LattPOSet L);
func % p -> Element of L equals :: LATTICE3:def 4
p;
correctness
coherence
p is Element of L;
;
end;

:: deftheorem defines % LATTICE3:def 4 :
for L being Lattice
for p being Element of (LattPOSet L) holds % p = p;

theorem Th7: :: LATTICE3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p, q being Element of L holds
( p [= q iff p % <= q % )
proof end;

definition
let X be set ;
let O be Order of X;
:: original: ~
redefine func O ~ -> Order of X;
coherence
O ~ is Order of X
proof end;
end;

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

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

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

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

theorem :: LATTICE3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being RelStr holds (A ~ ) ~ = RelStr(# the carrier of A,the InternalRel of A #) ;

definition
let A be RelStr ;
let a be Element of A;
func a ~ -> Element of (A ~ ) equals :: LATTICE3:def 6
a;
correctness
coherence
a is Element of (A ~ );
;
end;

:: deftheorem defines ~ LATTICE3:def 6 :
for A being RelStr
for a being Element of A holds a ~ = a;

definition
let A be RelStr ;
let a be Element of (A ~ );
func ~ a -> Element of A equals :: LATTICE3:def 7
a;
correctness
coherence
a is Element of A;
;
end;

:: deftheorem defines ~ LATTICE3:def 7 :
for A being RelStr
for a being Element of (A ~ ) holds ~ a = a;

theorem Th9: :: LATTICE3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being RelStr
for a, b being Element of A holds
( a <= b iff b ~ <= a ~ )
proof end;

definition
let A be RelStr ;
let X be set ;
let a be Element of A;
pred a is_<=_than X means :: LATTICE3:def 8
for b being Element of A st b in X holds
a <= b;
pred X is_<=_than a means :Def9: :: LATTICE3:def 9
for b being Element of A st b in X holds
b <= a;
end;

:: deftheorem defines is_<=_than LATTICE3:def 8 :
for A being RelStr
for X being set
for a being Element of A holds
( a is_<=_than X iff for b being Element of A st b in X holds
a <= b );

:: deftheorem Def9 defines is_<=_than LATTICE3:def 9 :
for A being RelStr
for X being set
for a being Element of A holds
( X is_<=_than a iff for b being Element of A st b in X holds
b <= a );

notation
let A be RelStr ;
let X be set ;
let a be Element of A;
synonym X is_>=_than a for a is_<=_than X;
synonym a is_>=_than X for X is_<=_than a;
end;

definition
let IT be RelStr ;
attr IT is with_suprema means :Def10: :: LATTICE3:def 10
for x, y being Element of IT ex z being Element of IT st
( x <= z & y <= z & ( for z' being Element of IT st x <= z' & y <= z' holds
z <= z' ) );
attr IT is with_infima means :Def11: :: LATTICE3:def 11
for x, y being Element of IT ex z being Element of IT st
( z <= x & z <= y & ( for z' being Element of IT st z' <= x & z' <= y holds
z' <= z ) );
end;

:: deftheorem Def10 defines with_suprema LATTICE3:def 10 :
for IT being RelStr holds
( IT is with_suprema iff for x, y being Element of IT ex z being Element of IT st
( x <= z & y <= z & ( for z' being Element of IT st x <= z' & y <= z' holds
z <= z' ) ) );

:: deftheorem Def11 defines with_infima LATTICE3:def 11 :
for IT being RelStr holds
( IT is with_infima iff for x, y being Element of IT ex z being Element of IT st
( z <= x & z <= y & ( for z' being Element of IT st z' <= x & z' <= y holds
z' <= z ) ) );

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 :: LATTICE3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being RelStr holds
( A is with_suprema iff A ~ is with_infima )
proof end;

theorem :: LATTICE3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice holds
( LattPOSet L is with_suprema & LattPOSet L is with_infima )
proof end;

definition
let IT be RelStr ;
attr IT is complete means :Def12: :: LATTICE3:def 12
for X being set ex a being Element of IT st
( X is_<=_than a & ( for b being Element of IT st X is_<=_than b holds
a <= b ) );
end;

:: deftheorem Def12 defines complete LATTICE3:def 12 :
for IT being RelStr holds
( IT is complete iff for X being set ex a being Element of IT st
( X is_<=_than a & ( for b being Element of IT st X is_<=_than b holds
a <= b ) ) );

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty RelStr st A is complete holds
( A is with_suprema & A 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 A be RelStr ;
assume A1: A is antisymmetric ;
let a, b be Element of A;
assume A2: ex x being Element of A st
( a <= x & b <= x & ( for c being Element of A st a <= c & b <= c holds
x <= c ) ) ;
func a "\/" b -> Element of A means :Def13: :: LATTICE3:def 13
( a <= it & b <= it & ( for c being Element of A st a <= c & b <= c holds
it <= c ) );
existence
ex b1 being Element of A st
( a <= b1 & b <= b1 & ( for c being Element of A st a <= c & b <= c holds
b1 <= c ) ) by A2;
uniqueness
for b1, b2 being Element of A st a <= b1 & b <= b1 & ( for c being Element of A st a <= c & b <= c holds
b1 <= c ) & a <= b2 & b <= b2 & ( for c being Element of A st a <= c & b <= c holds
b2 <= c ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines "\/" LATTICE3:def 13 :
for A being RelStr st A is antisymmetric holds
for a, b being Element of A st ex x being Element of A st
( a <= x & b <= x & ( for c being Element of A st a <= c & b <= c holds
x <= c ) ) holds
for b4 being Element of A holds
( b4 = a "\/" b iff ( a <= b4 & b <= b4 & ( for c being Element of A st a <= c & b <= c holds
b4 <= c ) ) );

Lm1: now
let A be non empty antisymmetric with_suprema RelStr ; :: thesis: for a, b, c being Element of A holds
( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds
c <= d ) ) )
let a, b be Element of A; :: thesis: for c being Element of A holds
( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds
c <= d ) ) )
ex x being Element of A st
( a <= x & b <= x & ( for c being Element of A st a <= c & b <= c holds
x <= c ) ) by Def10;
hence for c being Element of A holds
( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds
c <= d ) ) ) by Def13; :: thesis: verum
end;

definition
let A be RelStr ;
assume A1: A is antisymmetric ;
let a, b be Element of A;
assume A2: ex x being Element of A st
( a >= x & b >= x & ( for c being Element of A st a >= c & b >= c holds
x >= c ) ) ;
func a "/\" b -> Element of A means :Def14: :: LATTICE3:def 14
( it <= a & it <= b & ( for c being Element of A st c <= a & c <= b holds
c <= it ) );
existence
ex b1 being Element of A st
( b1 <= a & b1 <= b & ( for c being Element of A st c <= a & c <= b holds
c <= b1 ) ) by A2;
uniqueness
for b1, b2 being Element of A st b1 <= a & b1 <= b & ( for c being Element of A st c <= a & c <= b holds
c <= b1 ) & b2 <= a & b2 <= b & ( for c being Element of A st c <= a & c <= b holds
c <= b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines "/\" LATTICE3:def 14 :
for A being RelStr st A is antisymmetric holds
for a, b being Element of A st ex x being Element of A st
( a >= x & b >= x & ( for c being Element of A st a >= c & b >= c holds
x >= c ) ) holds
for b4 being Element of A holds
( b4 = a "/\" b iff ( b4 <= a & b4 <= b & ( for c being Element of A st c <= a & c <= b holds
c <= b4 ) ) );

Lm2: now
let A be non empty antisymmetric with_infima RelStr ; :: thesis: for a, b, c being Element of A holds
( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds
c >= d ) ) )
let a, b be Element of A; :: thesis: for c being Element of A holds
( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds
c >= d ) ) )
ex x being Element of A st
( a >= x & b >= x & ( for c being Element of A st a >= c & b >= c holds
x >= c ) ) by Def11;
hence for c being Element of A holds
( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds
c >= d ) ) ) by Def14; :: thesis: verum
end;

theorem Th13: :: LATTICE3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being antisymmetric with_suprema RelStr
for u1, u2 being Element of V holds u1 "\/" u2 = u2 "\/" u1
proof end;

theorem Th14: :: LATTICE3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being antisymmetric with_suprema RelStr
for u1, u2, u3 being Element of V st V is transitive holds
(u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3)
proof end;

theorem Th15: :: LATTICE3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being antisymmetric with_infima RelStr
for n1, n2 being Element of N holds n1 "/\" n2 = n2 "/\" n1
proof end;

theorem Th16: :: LATTICE3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being antisymmetric with_infima RelStr
for n1, n2, n3 being Element of N st N is transitive holds
(n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3)
proof end;

definition
let L be antisymmetric with_infima RelStr ;
let x, y be Element of L;
:: original: "/\"
redefine func x "/\" y -> Element of L;
commutativity
for x, y being Element of L holds x "/\" y = y "/\" x by Th15;
end;

definition
let L be antisymmetric with_suprema RelStr ;
let x, y be Element of L;
:: original: "\/"
redefine func x "\/" y -> Element of L;
commutativity
for x, y being Element of L holds x "\/" y = y "\/" x by Th13;
end;

theorem Th17: :: LATTICE3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being reflexive antisymmetric with_suprema with_infima RelStr
for k1, k2 being Element of K holds (k1 "/\" k2) "\/" k2 = k2
proof end;

theorem Th18: :: LATTICE3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being reflexive antisymmetric with_suprema with_infima RelStr
for k1, k2 being Element of K holds k1 "/\" (k1 "\/" k2) = k1
proof end;

theorem Th19: :: LATTICE3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being with_suprema with_infima Poset ex L being strict Lattice st RelStr(# the carrier of A,the InternalRel of A #) = LattPOSet L
proof end;

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

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

theorem :: LATTICE3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice holds
( (LattRel L) ~ = LattRel (L .: ) & (LattPOSet L) ~ = LattPOSet (L .: ) )
proof end;

definition
let L be non empty LattStr ;
let p be Element of L;
let X be set ;
pred p is_less_than X means :Def16: :: LATTICE3:def 16
for q being Element of L st q in X holds
p [= q;
pred X is_less_than p means :Def17: :: LATTICE3:def 17
for q being Element of L st q in X holds
q [= p;
end;

:: deftheorem Def16 defines is_less_than LATTICE3:def 16 :
for L being non empty LattStr
for p being Element of L
for X being set holds
( p is_less_than X iff for q being Element of L st q in X holds
p [= q );

:: deftheorem Def17 defines is_less_than LATTICE3:def 17 :
for L being non empty LattStr
for p being Element of L
for X being set holds
( X is_less_than p iff for q being Element of L st q in X holds
q [= p );

notation
let L be non empty LattStr ;
let p be Element of L;
let X be set ;
synonym X is_great_than p for p is_less_than X;
synonym p is_great_than X for X is_less_than p;
end;

theorem :: LATTICE3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p, q, r being Element of L holds
( p is_less_than {q,r} iff p [= q "/\" r )
proof end;

theorem :: LATTICE3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p, q, r being Element of L holds
( p is_great_than {q,r} iff q "\/" r [= p )
proof end;

definition
let IT be non empty LattStr ;
attr IT is complete means :Def18: :: LATTICE3:def 18
for X being set ex p being Element of IT st
( X is_less_than p & ( for r being Element of IT st X is_less_than r holds
p [= r ) );
attr IT is \/-distributive means :Def19: :: LATTICE3:def 19
for X being set
for a, b, c being Element of IT st X is_less_than a & ( for d being Element of IT st X is_less_than d holds
a [= d ) & { (b "/\" a') where a' is Element of IT : a' in X } is_less_than c & ( for d being Element of IT st { (b "/\" a') where a' is Element of IT : a' in X } is_less_than d holds
c [= d ) holds
b "/\" a [= c;
attr IT is /\-distributive means :: LATTICE3:def 20
for X being set
for a, b, c being Element of IT st X is_great_than a & ( for d being Element of IT st X is_great_than d holds
d [= a ) & { (b "\/" a') where a' is Element of IT : a' in X } is_great_than c & ( for d being Element of IT st { (b "\/" a') where a' is Element of IT : a' in X } is_great_than d holds
d [= c ) holds
c [= b "\/" a;
end;

:: deftheorem Def18 defines complete LATTICE3:def 18 :
for IT being non empty LattStr holds
( IT is complete iff for X being set ex p being Element of IT st
( X is_less_than p & ( for r being Element of IT st X is_less_than r holds
p [= r ) ) );

:: deftheorem Def19 defines \/-distributive LATTICE3:def 19 :
for IT being non empty LattStr holds
( IT is \/-distributive iff for X being set
for a, b, c being Element of IT st X is_less_than a & ( for d being Element of IT st X is_less_than d holds
a [= d ) & { (b "/\" a') where a' is Element of IT : a' in X } is_less_than c & ( for d being Element of IT st { (b "/\" a') where a' is Element of IT : a' in X } is_less_than d holds
c [= d ) holds
b "/\" a [= c );

:: deftheorem defines /\-distributive LATTICE3:def 20 :
for IT being non empty LattStr holds
( IT is /\-distributive iff for X being set
for a, b, c being Element of IT st X is_great_than a & ( for d being Element of IT st X is_great_than d holds
d [= a ) & { (b "\/" a') where a' is Element of IT : a' in X } is_great_than c & ( for d being Element of IT st { (b "\/" a') where a' is Element of IT : a' in X } is_great_than d holds
d [= c ) holds
c [= b "\/" a );

theorem :: LATTICE3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for B being B_Lattice
for a being Element of B holds
( X is_less_than a iff { (b ` ) where b is Element of B : b in X } is_great_than a ` )
proof end;

theorem Th24: :: LATTICE3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for B being B_Lattice
for a being Element of B holds
( X is_great_than a iff { (b ` ) where b is Element of B : b in X } is_less_than a ` )
proof end;

theorem Th25: :: LATTICE3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds BooleLatt X is complete
proof end;

theorem Th26: :: LATTICE3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds BooleLatt X is \/-distributive
proof end;

theorem Th27: :: LATTICE3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds BooleLatt X 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being Lattice
for p being Element of L holds
( p is_less_than X iff p % is_<=_than X )
proof end;

theorem :: LATTICE3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being Lattice
for p' being Element of (LattPOSet L) holds
( p' is_<=_than X iff % p' is_less_than X )
proof end;

theorem Th30: :: LATTICE3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being Lattice
for p being Element of L holds
( X is_less_than p iff X is_<=_than p % )
proof end;

theorem Th31: :: LATTICE3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being Lattice
for p' being Element of (LattPOSet L) holds
( X is_<=_than p' iff X is_less_than % p' )
proof end;

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

definition
let L be non empty LattStr ;
assume A1: L is complete Lattice ;
let X be set ;
func "\/" X,L -> Element of L means :Def21: :: LATTICE3:def 21
( X is_less_than it & ( for r being Element of L st X is_less_than r holds
it [= r ) );
existence
ex b1 being Element of L st
( X is_less_than b1 & ( for r being Element of L st X is_less_than r holds
b1 [= r ) ) by A1, Def18;
uniqueness
for b1, b2 being Element of L st X is_less_than b1 & ( for r being Element of L st X is_less_than r holds
b1 [= r ) & X is_less_than b2 & ( for r being Element of L st X is_less_than r holds
b2 [= r ) holds
b1 = b2
proof end;
end;

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

definition
let L be non empty LattStr ;
let X be set ;
func "/\" X,L -> Element of L equals :: LATTICE3:def 22
 "\/" { p where p is Element of L : p is_less_than X } ,L;
correctness
coherence
"\/" { p where p is Element of L : p is_less_than X } ,L is Element of L;
;
end;

:: deftheorem defines "/\" LATTICE3:def 22 :
for L being non empty LattStr
for X being set holds "/\" X,L = "\/" { p where p is Element of L : p is_less_than X } ,L;

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

theorem Th32: :: LATTICE3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice
for a being Element of C
for X being set holds "\/" { (a "/\" b) where b is Element of C : b in X } ,C [= a "/\" ("\/" X,C)
proof end;

theorem Th33: :: LATTICE3:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice holds
( C is \/-distributive iff for X being set
for a being Element of C holds a "/\" ("\/" X,C) [= "\/" { (a "/\" b) where b is Element of C : b in X } ,C )
proof end;

theorem Th34: :: LATTICE3:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice
for a being Element of C
for X being set holds
( a = "/\" X,C iff ( a is_less_than X & ( for b being Element of C st b is_less_than X holds
b [= a ) ) )
proof end;

theorem Th35: :: LATTICE3:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice
for a being Element of C
for X being set holds a "\/" ("/\" X,C) [= "/\" { (a "\/" b) where b is Element of C : b in X } ,C
proof end;

theorem Th36: :: LATTICE3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice holds
( C is /\-distributive iff for X being set
for a being Element of C holds "/\" { (a "\/" b) where b is Element of C : b in X } ,C [= a "\/" ("/\" X,C) )
proof end;

theorem :: LATTICE3:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice
for X being set holds "\/" X,C = "/\" { a where a is Element of C : a is_great_than X } ,C
proof end;

theorem Th38: :: LATTICE3:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice
for a being Element of C
for X being set st a in X holds
( a [= "\/" X,C & "/\" X,C [= a )
proof end;

theorem :: LATTICE3:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th40: :: LATTICE3:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice
for a being Element of C
for X being set st a is_less_than X holds
a [= "/\" X,C
proof end;

theorem Th41: :: LATTICE3:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice
for a being Element of C
for X being set st a in X & X is_less_than a holds
"\/" X,C = a
proof end;

theorem Th42: :: LATTICE3:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice
for a being Element of C
for X being set st a in X & a is_less_than X holds
"/\" X,C = a
proof end;

theorem :: LATTICE3:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice
for a being Element of C holds
( "\/" {a} = a & "/\" {a} = a )
proof end;

theorem :: LATTICE3:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice
for a, b being Element of C holds
( a "\/" b = "\/" {a,b} & a "/\" b = "/\" {a,b} )
proof end;

theorem :: LATTICE3:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice
for a being Element of C holds
( a = "\/" { b where b is Element of C : b [= a } ,C & a = "/\" { c where c is Element of C : a [= c } ,C )
proof end;

theorem Th46: :: LATTICE3:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice
for X, Y being set st X c= Y holds
( "\/" X,C [= "\/" Y,C & "/\" Y,C [= "/\" X,C )
proof end;

theorem Th47: :: LATTICE3:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice
for X being set holds
( "\/" X,C = "\/" { a where a is Element of C : ex b being Element of C st
( a [= b & b in X ) } ,C & "/\" X,C = "/\" { b where b is Element of C : ex a being Element of C st
( a [= b & a in X ) } ,C )
proof end;

theorem :: LATTICE3:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice
for X, Y being set st ( for a being Element of C st a in X holds
ex b being Element of C st
( a [= b & b in Y ) ) holds
"\/" X,C [= "\/" Y,C
proof end;

theorem :: LATTICE3:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice
for X being set st X c= bool the carrier of C holds
"\/" (union X),C = "\/" { ("\/" Y) where Y is Subset of C : Y in X } ,C
proof end;

theorem :: LATTICE3:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice holds
( C is 0_Lattice & Bottom C = "\/" {} ,C )
proof end;

theorem :: LATTICE3:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice holds
( C is 1_Lattice & Top C = "\/" the carrier of C,C )
proof end;

theorem Th52: :: LATTICE3:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice
for a, b being Element of C st C is I_Lattice holds
a => b = "\/" { c where c is Element of C : a "/\" c [= b } ,C
proof end;

theorem :: LATTICE3:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being complete Lattice st C is I_Lattice holds
C is \/-distributive
proof end;

theorem :: LATTICE3:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for D being complete \/-distributive Lattice
for a being Element of D holds
( a "/\" ("\/" X,D) = "\/" { (a "/\" b1) where b1 is Element of D : b1 in X } ,D & ("\/" X,D) "/\" a = "\/" { (b2 "/\" a) where b2 is Element of D : b2 in X } ,D )
proof end;

theorem :: LATTICE3:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for D being complete /\-distributive Lattice
for a being Element of D holds
( a "\/" ("/\" X,D) = "/\" { (a "\/" b1) where b1 is Element of D : b1 in X } ,D & ("/\" X,D) "\/" a = "/\" { (b2 "\/" a) where b2 is Element of D : b2 in X } ,D )
proof end;

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

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

Lm3: now
let D be non empty set ; :: thesis: for f being Function of bool D,D st ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) holds
ex L being strict Lattice st
( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) )
let f be Function of bool D,D; :: thesis: ( ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) implies ex L being strict Lattice st
( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) ) )
assume that
A1: for a being Element of D holds f . {a} = a and
A2: for X being Subset-Family of D holds f . (f .: X) = f . (union X) ; :: thesis: ex L being strict Lattice st
( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) )
defpred S1[ set , set ] means f . {$1,$2} = $2;
consider R being Relation of D such that
A3: for x, y being set holds
( [x,y] in R iff ( x in D & y in D & S1[x,y] ) ) from RELSET_1:sch 1( D D );
A4: dom f = bool D by FUNCT_2:def 1;
A5: now
let x, y be Subset of D; :: thesis: f . {(f . x),(f . y)} = f . (x \/ y)
thus f . {(f . x),(f . y)} = f . (f .: {x,y}) by A4, FUNCT_1:118
.= f . (union {x,y}) by A2
.= f . (x \/ y) by ZFMISC_1:93 ; :: thesis: verum
end;
A6: for x, y being Element of D
for X being Subset of D st y in X holds
f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X }
proof
let x, y be Element of D; :: thesis: for X being Subset of D st y in X holds
f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X }
let X be Subset of D; :: thesis: ( y in X implies f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X } )
assume A7: y in X ; :: thesis: f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X }
set Y = { {t,x} where t is Element of D : t in X } ;
A8: X \/ {x} = union { {t,x} where t is Element of D : t in X }
proof
thus X \/ {x} c= union { {t,x} where t is Element of D : t in X } :: according to XBOOLE_0:def 10 :: thesis: union { {t,x} where t is Element of D : t in X } c= X \/ {x}
proof
let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in X \/ {x} or s in union { {t,x} where t is Element of D : t in X } )
assume s in X \/ {x} ; :: thesis: s in union { {t,x} where t is Element of D : t in X }
then ( ( s in X & X c= D ) or s in {x} ) by XBOOLE_0:def 2;
then ( ( s in X & s is Element of D ) or s = x ) by TARSKI:def 1;
then ( ( s in {s,x} & {s,x} in { {t,x} where t is Element of D : t in X } ) or ( s in {y,x} & {y,x} in { {t,x} where t is Element of D : t in X } ) ) by A7, TARSKI:def 2;
hence s in union { {t,x} where t is Element of D : t in X } by TARSKI:def 4; :: thesis: verum
end;
let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in union { {t,x} where t is Element of D : t in X } or s in X \/ {x} )
assume s in union { {t,x} where t is Element of D : t in X } ; :: thesis: s in X \/ {x}
then consider Z being set such that
A9: ( s in Z & Z in { {t,x} where t is Element of D : t in X } ) by TARSKI:def 4;
consider t being Element of D such that
A10: ( Z = {t,x} & t in X ) by A9;
( s = t or ( s = x & x in {x} ) ) by A9, A10, TARSKI:def 1, TARSKI:def 2;
hence s in X \/ {x} by A10, XBOOLE_0:def 2; :: thesis: verum
end;
{ {t,x} where t is Element of D : t in X } c= bool D
proof
let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in { {t,x} where t is Element of D : t in X } or s in bool D )
assume s in { {t,x} where t is Element of D : t in X } ; :: thesis: s in bool D
then ( s c= X \/ {x} & X \/ {x} c= D ) by A8, ZFMISC_1:92;
then s c= D by XBOOLE_1:1;
hence s in bool D ; :: thesis: verum
end;
then reconsider Y = { {t,x} where t is Element of D : t in X } as Subset-Family of D ;
defpred S2[ set ] means $1 in X;
deffunc H4( Element of D) -> Element of bool D = {$1,x};
A11: bool D c= dom f by FUNCT_2:def 1;
f .: { H4(t) where t is Element of D : S2[t] } = { (f . H4(t)) where t is Element of D : S2[t] } from LATTICE3:sch 2( D bool D f , A11);
 then f . (union Y) = f . { (f . {t,x}) where t is Element of D : t in X } by A2;
hence f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X } by A8; :: thesis: verum
end;
A12: R is_reflexive_in D
proof
let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in D or [x,x] in R )
assume A13: x in D ; :: thesis: [x,x] in R
then x = f . {x} by A1
.= f . {x,x} by ENUMSET1:69 ;
hence [x,x] in R by A3, A13; :: thesis: verum
end;
A14: R is_antisymmetric_in D
proof
let x, y be set ; :: according to RELAT_2:def 4 :: thesis: ( not x in D or not y in D or not [x,y] in R or not [y,x] in R or x = y )
assume ( x in D & y in D & [x,y] in R & [y,x] in R ) ; :: thesis: x = y
then ( f . {x,y} = y & f . {y,x} = x ) by A3;
hence x = y ; :: thesis: verum
end;
A15: R is_transitive_in D
proof
let x, y, z be set ; :: according to RELAT_2:def 8 :: thesis: ( not x in D or not y in D or not z in D or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume A16: ( x in D & y in D & z in D & [x,y] in R & [y,z] in R ) ; :: thesis: [x,z] in R
then reconsider a = x, b = y, c = z as Element of D ;
A17: ( f . {x,y} = y & f . {y,z} = z ) by A3, A16;
then f . {a,c} = f . {(f . {a}),(f . {b,c})} by A1
.= f . ({a} \/ {b,c}) by A5
.= f . {a,b,c} by ENUMSET1:42
.= f . ({a,b} \/ {c}) by ENUMSET1:43
.= f . {(f . {a,b}),(f . {c})} by A5
.= c by A1, A17 ;
hence [x,z] in R by A3; :: thesis: verum
end;
A18: dom R = D by A12, ORDERS_1:98;
field R = D by A12, ORDERS_1:98;
then reconsider R = R as Order of D by A12, A14, A15, A18, PARTFUN1:def 4, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;
set A = RelStr(# D,R #);
RelStr(# D,R #) is complete
proof
let X be set ; :: according to LATTICE3:def 12 :: thesis: ex a being Element of RelStr(# D,R #) st
( X is_<=_than a & ( for b being Element of RelStr(# D,R #) st X is_<=_than b holds
a <= b ) )
reconsider Y = X /\ D as Subset of D by XBOOLE_1:17;
reconsider a = f . Y as Element of RelStr(# D,R #) ;
take a ; :: thesis: ( X is_<=_than a & ( for b being Element of RelStr(# D,R #) st X is_<=_than b holds
a <= b ) )
thus X is_<=_than a :: thesis: for b being Element of RelStr(# D,R #) st X is_<=_than b holds
a <= b
proof
let b be Element of RelStr(# D,R #); :: according to LATTICE3:def 9 :: thesis: ( b in X implies b <= a )
assume b in X ; :: thesis: b <= a
then b in Y by XBOOLE_0:def 3;
then {b} \/ Y = Y by ZFMISC_1:46;
then a = f . {(f . {b}),a} by A5
.= f . {b,a} by A1 ;
hence [b,a] in the InternalRel of RelStr(# D,R #) by A3; :: according to ORDERS_2:def 9 :: thesis: verum
end;
let b be Element of RelStr(# D,R #); :: thesis: ( X is_<=_than b implies a <= b )
assume A19: X is_<=_than b ; :: thesis: a <= b
A20: f . {a,b} = f . {a,(f . {b})} by A1
.= f . (Y \/ {b}) by A5 ;
now
per cases ( Y <> {} or Y = {} ) ;
suppose A21: Y <> {} ; :: thesis: f . {a,b} = b
consider s being Element of Y;
reconsider s = s as Element of D by A21, TARSKI:def 3;
deffunc H4( Element of D) -> set = f . {$1,b};
deffunc H5( Element of D) -> Element of RelStr(# D,R #) = b;
defpred S2[ set ] means $1 in Y;
A22: for t being Element of D st S2[t] holds
H4(t) = H5(t)
proof
let t be Element of D; :: thesis: ( S2[t] implies H4(t) = H5(t) )
reconsider s = t as Element of RelStr(# D,R #) ;
reconsider y = b as Element of D ;
assume t in Y ; :: thesis: H4(t) = H5(t)
then t in X by XBOOLE_0:def 3;
then s <= b by A19, Def9;
then [t,y] in R by ORDERS_2:def 9;
hence H4(t) = H5(t) by A3; :: thesis: verum
end;
A23: s in Y by A21;
then A24: ex t being Element of D st S2[t] ;
{ H4(t) where t is Element of D : S2[t] } = { H5(t) where t is Element of D : S2[t] } from FRAENKEL:sch 6( D , A22)
.= { b where t is Element of D : S2[t] }
.= {b} from LATTICE3:sch 1( Y D , A24) ;
hence f . {a,b} = f . {b} by A6, A20, A23
.= b by A1 ;
:: thesis: verum
end;
suppose Y = {} ; :: thesis: f . {a,b} = b
hence f . {a,b} = b by A1, A20; :: thesis: verum
end;
end;
end;
hence [a,b] in the InternalRel of RelStr(# D,R #) by A3; :: according to ORDERS_2:def 9 :: thesis: verum
end;
then reconsider A = RelStr(# D,R #) as non empty strict complete Poset ;
take L = latt A; :: thesis: ( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) )
A25: ( A is with_suprema & A is with_infima ) by Th12;
then A26: ( A = LattPOSet L & LattPOSet L = RelStr(# H1(L),(LattRel L) #) ) by Def15;
hence H1(L) = D ; :: thesis: for X being Subset of L holds "\/" X = f . X
let X be Subset of L; :: thesis: "\/" X = f . X
reconsider Y = X as Subset of D by A26;
reconsider a = f . Y as Element of (LattPOSet L) by A25, Def15;
set p = % a;
X is_<=_than a
proof
let b be Element of (LattPOSet L); :: according to LATTICE3:def 9 :: thesis: ( b in X implies b <= a )
reconsider y = b as Element of D by A25, Def15;
assume b in X ; :: thesis: b <= a
then A27: X = {b} \/ X by ZFMISC_1:46;
f . {y,(f . Y)} = f . {(f . {y}),(f . Y)} by A1
.= a by A5, A27 ;
hence [b,a] in the InternalRel of (LattPOSet L) by A3, A26; :: according to ORDERS_2:def 9 :: thesis: verum
end;
then A28: X is_less_than % a by Th31;
now
let q be Element of L; :: thesis: ( X is_less_than q implies % a [= q )
reconsider y = q as Element of D by A26;
reconsider b = y as Element of (LattPOSet L) ;
assume X is_less_than q ; :: thesis: % a [= q
then A29: ( X is_<=_than q % & b = q % ) by Th30;
A30: f . {(f . Y),b} = f . {(f . Y),(f . {y})} by A1
.= f . (Y \/ {b}) by A5 ;
now
per cases ( Y <> {} or Y = {} ) ;
suppose A31: Y <> {} ; :: thesis: f . {a,b} = b
consider s being Element of Y;
reconsider s = s as Element of D by A31, TARSKI:def 3;
deffunc H4( Element of D) -> set = f . {$1,b};
deffunc H5( Element of D) -> Element of (LattPOSet L) = b;
defpred S2[ set ] means $1 in Y;
A32: for t being Element of D st S2[t] holds
H4(t) = H5(t)
proof
let t be Element of D; :: thesis: ( S2[t] implies H4(t) = H5(t) )
reconsider s = t as Element of (LattPOSet L) by A25, Def15;
assume t in Y ; :: thesis: H4(t) = H5(t)
then s <= b by A29, Def9;
then [t,y] in R by A26, ORDERS_2:def 9;
hence H4(t) = H5(t) by A3; :: thesis: verum
end;
A33: s in Y by A31;
then A34: ex t being Element of D st S2[t] ;
{ H4(t) where t is Element of D : S2[t] } = { H5(t) where t is Element of D : S2[t] } from FRAENKEL:sch 6( D , A32)
.= { b where t is Element of D : S2[t] }
.= {b} from LATTICE3:sch 1( b D , A34) ;
hence f . {a,b} = f . {b} by A6, A30, A33
.= b by A1 ;
:: thesis: verum
end;
suppose Y = {} ; :: thesis: f . {a,b} = b
hence f . {a,b} = b by A1, A30; :: thesis: verum
end;
end;
end;
then [a,b] in the InternalRel of (LattPOSet L) by A3, A26;
then ( a <= b & (% a) % = % a & a = % a & q % = b ) by ORDERS_2:def 9;
hence % a [= q by Th7; :: thesis: verum
end;
hence "\/" X = % a by A28, Def21
.= f . X ;
:: thesis: verum
end;

theorem :: LATTICE3:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f being Function of bool D,D st ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) holds
ex L being strict complete Lattice st
( the carrier of L = D & ( for X being Subset of L holds "\/" X = f . X ) ) by Lm3;