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 by YELLOW_0:17, Th31;
then Ex is directed-sups-preserving ;
hence "\/" (F,(T |^ the carrier of S)) in the carrier of (ContMaps (S,T)) by Def3; :: thesis: verum