let X be non empty TopSpace; :: thesis: for L being non empty up-complete Scott TopPoset holds ContMaps X,L is directed-sups-inheriting SubRelStr of L |^ the carrier of X
let L be non empty up-complete Scott TopPoset; :: thesis: ContMaps X,L is directed-sups-inheriting SubRelStr of L |^ the carrier of X
reconsider XL = ContMaps X,L as non empty full SubRelStr of L |^ the carrier of X by WAYBEL24:def 3;
XL is directed-sups-inheriting

proof

let A be directed Subset of XL; :: according to WAYBEL_0:def 4 :: thesis: ( A = {} or not ex_sup_of A,L |^ the carrier of X or "\/" A,(L |^ the carrier of X) in the carrier of XL )
assume ( A <> {} & ex_sup_of A,L |^ the carrier of X ) ; :: thesis: "\/" A,(L |^ the carrier of X) in the carrier of XL
then reconsider A = A as non empty directed Subset of XL ;
"\/" A,(L |^ the carrier of X) is continuous Function of X,L by Th11;
hence "\/" A,(L |^ the carrier of X) in the carrier of XL by WAYBEL24:def 3; :: thesis: verum

end;

hence ContMaps X,L is directed-sups-inheriting SubRelStr of L |^ the carrier of X ; :: thesis: verum