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 X9 = X as non empty directed Subset of S ;
Ex preserves_sup_of X9

proof

assume ex_sup_of X9,S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of Ex .: X9,T & "\/" ((Ex .: X9),T) = Ex . ("\/" (X9,S)) )
thus ex_sup_of Ex .: X9,T by YELLOW_0:17; :: thesis: "\/" ((Ex .: X9),T) = Ex . ("\/" (X9,S))
thus "\/" ((Ex .: X9),T) = Ex . ("\/" (X9,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;
hence "\/" (F,(T |^ the carrier of S)) in the carrier of (ContMaps (S,T)) by Def3; :: thesis: verum