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