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

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

hence
ContMaps (X,L) is directed-sups-inheriting SubRelStr of L |^ the carrier of X
; :: thesis: verum
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;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