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 S₁[ 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 : S₁[X] } ;
{ (sup X) where X is non empty directed Subset of L : S₁[X] } c= the carrier of L

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { (sup X) where X is non empty directed Subset of L : S₁[X] } or q in the carrier of L )
assume q in { (sup X) where X is non empty directed Subset of L : S₁[X] } ; :: thesis: q in the carrier of L
then consider X being non empty directed Subset of L such that
A1: ( q = sup X & S₁[X] ) ;
thus q in the carrier of L by A1; :: thesis: verum

end;

then reconsider A = { (sup X) where X is non empty directed Subset of L : S₁[X] } as Subset of L ;
set R = { X where X is non empty directed Subset of L : S₁[X] } ;
union { X where X is non empty directed Subset of L : S₁[X] } c= the carrier of L

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in union { X where X is non empty directed Subset of L : S₁[X] } or q in the carrier of L )
assume q in union { X where X is non empty directed Subset of L : S₁[X] } ; :: thesis: q in the carrier of L
then consider r being set such that
A2: ( q in r & r in { X where X is non empty directed Subset of L : S₁[X] } ) by TARSKI:def 4;
consider s being non empty directed Subset of L such that
A3: ( r = s & ex x being Element of L st
( s = {x} "/\" D2 & x in D1 ) ) by A2;
thus q in the carrier of L by A2, A3; :: thesis: verum

end;

then reconsider UR = union { X where X is non empty directed Subset of L : S₁[X] } as Subset of L ;
set a = sup UR;
A4: ex_sup_of UR,L by Th7;
A5: 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
A6: ( b = sup X & S₁[X] ) ;
A7: ex_sup_of X,L by WAYBEL_0:75;
X in { X where X is non empty directed Subset of L : S₁[X] } by A6;
hence b <= sup UR by A4, A6, A7, YELLOW_0:34, ZFMISC_1:92; :: thesis: verum

end;

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 A8: 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
A9: k in k1 and
A10: k1 in { X where X is non empty directed Subset of L : S₁[X] } by TARSKI:def 4;
consider s being non empty directed Subset of L such that
A11: k1 = s and
A12: S₁[s] by A10;
consider x being Element of L such that
A13: ( s = {x} "/\" D2 & x in D1 ) by A12;
{x} "/\" D2 = { (x "/\" d2) where d2 is Element of L : d2 in D2 } by YELLOW_4:42;
then consider d2 being Element of L such that
A14: ( k = x "/\" d2 & d2 in D2 ) by A9, A11, A13;
sup s in A by A12;
then A15: sup s <= b by A8, LATTICE3:def 9;
x "/\" d2 <= sup s by A9, A11, A13, A14, Th1, YELLOW_4:1;
hence k <= b by A14, A15, YELLOW_0:def 2; :: thesis: verum

end;

hence sup UR <= b by A4, YELLOW_0:def 9; :: 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 A5, YELLOW_0:15; :: thesis: verum