let L be up-complete Semilattice; :: thesis: for D being non empty directed Subset of [:L,L:] holds "\/" { (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 <= "\/" (union { 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: "\/" { (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 <= "\/" (union { 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
defpred S₁[ set ] means ex x being Element of L st
( $1 = {x} "/\" (proj2 D) & x in proj1 D );
A1: ex_sup_of { (sup X) where X is non empty directed Subset of L : S₁[X] } ,L by Th8;
"\/" (union { X where X is non empty directed Subset of L : S₁[X] } ),L is_>=_than { (sup X) where X is non empty directed Subset of L : S₁[X] }

proof

let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in { (sup X) where X is non empty directed Subset of L : S₁[X] } or a <= "\/" (union { X where X is non empty directed Subset of L : S₁[X] } ),L )
assume a in { (sup X) where X is non empty directed Subset of L : S₁[X] } ; :: thesis: a <= "\/" (union { X where X is non empty directed Subset of L : S₁[X] } ),L
then consider q being non empty directed Subset of L such that
A2: ( a = sup q & S₁[q] ) ;
A3: ex_sup_of q,L by WAYBEL_0:75;
A4: ex_sup_of union { X where X is non empty directed Subset of L : S₁[X] } ,L by Th7;
q in { X where X is non empty directed Subset of L : S₁[X] } by A2;
hence a <= "\/" (union { X where X is non empty directed Subset of L : S₁[X] } ),L by A2, A3, A4, YELLOW_0:34, ZFMISC_1:92; :: thesis: verum

end;

hence "\/" { (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 <= "\/" (union { 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 A1, YELLOW_0:def 9; :: thesis: verum