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: 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 and
A4: 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
A5: b = c and
A6: S₁[c] by A4;
"\/" c,L in { ("\/" X,L) where X is non empty directed Subset of L : S₁[X] } by A6;
then A7: "\/" c,L <= "\/" { ("\/" X,L) where X is non empty directed Subset of L : S₁[X] } ,L by Th8, YELLOW_4:1;
ex_sup_of c,L by WAYBEL_0:75;
then a <= "\/" c,L by A3, A5, YELLOW_4:1;
hence a <= "\/" { ("\/" X,L) where X is non empty directed Subset of L : S₁[X] } ,L by A7, YELLOW_0:def 2; :: thesis: verum

end;

ex_sup_of union { X where X is non empty directed Subset of L : S₁[X] } ,L by Th7;
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