let L be up-complete Semilattice; :: thesis: for D being non empty directed Subset of [:L,L:] holds ex_sup_of { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L
let D be non empty directed Subset of [:L,L:]; :: thesis: ex_sup_of { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L
reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22;
defpred S1[ set ] means ex x being Element of L st
( $1 = {x} "/\" D2 & x in D1 );
set A = { (sup X) where X is non empty directed Subset of L : S1[X] } ;
{ (sup X) where X is non empty directed Subset of L : S1[X] } c= the carrier of L
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { (sup X) where X is non empty directed Subset of L : S1[X] } or q in the carrier of L )
assume q in { (sup X) where X is non empty directed Subset of L : S1[X] } ; :: thesis: q in the carrier of L
then ex X being non empty directed Subset of L st
( q = sup X & S1[X] ) ;
hence q in the carrier of L ; :: thesis: verum
end;
then reconsider A = { (sup X) where X is non empty directed Subset of L : S1[X] } as Subset of L ;
set R = { X where X is non empty directed Subset of L : S1[X] } ;
union { X where X is non empty directed Subset of L : S1[X] } c= the carrier of L
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in union { X where X is non empty directed Subset of L : S1[X] } or q in the carrier of L )
assume q in union { X where X is non empty directed Subset of L : S1[X] } ; :: thesis: q in the carrier of L
then consider r being set such that
A1: q in r and
A2: r in { X where X is non empty directed Subset of L : S1[X] } by TARSKI:def 4;
ex s being non empty directed Subset of L st
( r = s & ex x being Element of L st
( s = {x} "/\" D2 & x in D1 ) ) by A2;
hence q in the carrier of L by A1; :: thesis: verum
end;
then reconsider UR = union { X where X is non empty directed Subset of L : S1[X] } as Subset of L ;
set a = sup UR;
A3: ex_sup_of UR,L by Th7;
A4: for b being Element of L st A is_<=_than b holds
sup UR <= b
proof
let b be Element of L; :: thesis: ( A is_<=_than b implies sup UR <= b )
assume A5: A is_<=_than b ; :: thesis: sup UR <= b
UR is_<=_than b
proof
let k be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not k in UR or k <= b )
assume k in UR ; :: thesis: k <= b
then consider k1 being set such that
A6: k in k1 and
A7: k1 in { X where X is non empty directed Subset of L : S1[X] } by TARSKI:def 4;
consider s being non empty directed Subset of L such that
A8: k1 = s and
A9: S1[s] by A7;
consider x being Element of L such that
A10: s = {x} "/\" D2 and
x in D1 by A9;
A11: {x} "/\" D2 = { (x "/\" d2) where d2 is Element of L : d2 in D2 } by YELLOW_4:42;
sup s in A by A9;
then A12: sup s <= b by A5;
consider d2 being Element of L such that
A13: k = x "/\" d2 and
d2 in D2 by A6, A8, A10, A11;
x "/\" d2 <= sup s by A6, A8, A10, A13, Th1, YELLOW_4:1;
hence k <= b by A13, A12, YELLOW_0:def 2; :: thesis: verum
end;
hence sup UR <= b by A3, YELLOW_0:def 9; :: thesis: verum
end;
A is_<=_than sup UR
proof
let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in A or b <= sup UR )
assume b in A ; :: thesis: b <= sup UR
then consider X being non empty directed Subset of L such that
A14: b = sup X and
A15: S1[X] ;
 ( ex_sup_of X,L & X in { X where X is non empty directed Subset of L : S1[X] } ) by A15, WAYBEL_0:75;
hence b <= sup UR by A3, A14, YELLOW_0:34, ZFMISC_1:74; :: thesis: verum
end;
hence ex_sup_of { (sup X) where X is non empty directed Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } ,L by A4, YELLOW_0:15; :: thesis: verum