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: "\/" { (sup X) where X is non empty directed Subset of L : S₁[X] } ,L <= "\/" (union { X where X is non empty directed Subset of L : S₁[X] } ),L by Th9;
A2: ex_sup_of union { X where X is non empty directed Subset of L : S₁[X] } ,L by Th7;
union { X where X is non empty directed Subset of L : S₁[X] } is_<=_than "\/" { ("\/" X,L) where X is non empty directed Subset of L : S₁[X] } ,L

proof

let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in union { X where X is non empty directed Subset of L : S₁[X] } or a <= "\/" { ("\/" X,L) where X is non empty directed Subset of L : S₁[X] } ,L )
assume a in union { X where X is non empty directed Subset of L : S₁[X] } ; :: thesis: a <= "\/" { ("\/" X,L) where X is non empty directed Subset of L : S₁[X] } ,L
then consider b being set such that
A3: ( a in b & b in { X where X is non empty directed Subset of L : S₁[X] } ) by TARSKI:def 4;
consider c being non empty directed Subset of L such that
A4: ( b = c & S₁[c] ) by A3;
ex_sup_of c,L by WAYBEL_0:75;
then A5: a <= "\/" c,L by A3, A4, YELLOW_4:1;
"\/" c,L in { ("\/" X,L) where X is non empty directed Subset of L : S₁[X] } by A4;
then "\/" c,L <= "\/" { ("\/" X,L) where X is non empty directed Subset of L : S₁[X] } ,L by Th8, YELLOW_4:1;
hence a <= "\/" { ("\/" X,L) where X is non empty directed Subset of L : S₁[X] } ,L by A5, YELLOW_0:def 2; :: thesis: verum

end;

then "\/" (union { X where X is non empty directed Subset of L : S₁[X] } ),L <= "\/" { ("\/" X,L) where X is non empty directed Subset of L : S₁[X] } ,L by A2, YELLOW_0:def 9;
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, ORDERS_2:25; :: thesis: verum