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} "/\" () & 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} "/\" () & 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} "/\" () & 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} "/\" () & x in proj1 D )
}
)
,L)

defpred S1[ set ] means ex x being Element of L st
( \$1 = {x} "/\" () & 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] }
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 : S1[X] } or a <= "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) )
assume a in { (sup X) where X is non empty directed Subset of L : S1[X] } ; :: thesis: a <= "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L)
then consider q being non empty directed Subset of L such that
A2: a = sup q and
A3: S1[q] ;
A4: q in { X where X is non empty directed Subset of L : S1[X] } by A3;
( ex_sup_of q,L & ex_sup_of union { X where X is non empty directed Subset of L : S1[X] } ,L ) by ;
hence a <= "\/" ((union { X where X is non empty directed Subset of L : S1[X] } ),L) by ; :: thesis: verum
end;
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} "/\" () & 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} "/\" () & x in proj1 D )
}
)
,L) by ; :: thesis: verum