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 that
A1: A <> {} and
ex_sup_of A,L |^ the carrier of X ; :: thesis: "\/" (A,(L |^ the carrier of X)) in the carrier of XL
reconsider A = A as non empty directed Subset of XL by A1;
"\/" (A,(L |^ the carrier of X)) is continuous Function of X,L by Th8;
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