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:2; :: thesis: verum