let S, T be complete Scott TopLattice; :: thesis: for F being non empty Subset of (ContMaps S,T) holds "\/" F,(T |^ the carrier of S) in the carrier of (ContMaps S,T)
let F be non empty Subset of (ContMaps S,T); :: thesis: "\/" F,(T |^ the carrier of S) in the carrier of (ContMaps S,T)
reconsider Ex = "\/" F,(T |^ the carrier of S) as Function of S,T by Th19;
for X being Subset of S st not X is empty & X is directed holds
Ex preserves_sup_of X

proof

let X be Subset of S; :: thesis: ( not X is empty & X is directed implies Ex preserves_sup_of X )
assume ( not X is empty & X is directed ) ; :: thesis: Ex preserves_sup_of X
then reconsider X' = X as non empty directed Subset of S ;
Ex preserves_sup_of X'

proof

assume ex_sup_of X',S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of Ex .: X',T & "\/" (Ex .: X'),T = Ex . ("\/" X',S) )
thus ex_sup_of Ex .: X',T by YELLOW_0:17; :: thesis: "\/" (Ex .: X'),T = Ex . ("\/" X',S)
thus "\/" (Ex .: X'),T = Ex . ("\/" X',S) by Th31; :: thesis: verum

end;

hence Ex preserves_sup_of X ; :: thesis: verum

end;

then Ex is directed-sups-preserving by WAYBEL_0:def 37;
then Ex is continuous ;
hence "\/" F,(T |^ the carrier of S) in the carrier of (ContMaps S,T) by Def3; :: thesis: verum