let S, T be complete Scott TopLattice; :: thesis: UPS (S,T) = SCMaps (S,T)
A1: the carrier of (UPS (S,T)) = the carrier of (SCMaps (S,T))

proof

thus the carrier of (UPS (S,T)) c= the carrier of (SCMaps (S,T)) :: according to XBOOLE_0:def 10 :: thesis: the carrier of (SCMaps (S,T)) c= the carrier of (UPS (S,T))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (UPS (S,T)) or x in the carrier of (SCMaps (S,T)) )
assume x in the carrier of (UPS (S,T)) ; :: thesis: x in the carrier of (SCMaps (S,T))
then reconsider f = x as directed-sups-preserving Function of S,T by Def4;
f is continuous ;
hence x in the carrier of (SCMaps (S,T)) by WAYBEL17:def 2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (SCMaps (S,T)) or x in the carrier of (UPS (S,T)) )
assume A2: x in the carrier of (SCMaps (S,T)) ; :: thesis: x in the carrier of (UPS (S,T))
the carrier of (SCMaps (S,T)) c= the carrier of (MonMaps (S,T)) by YELLOW_0:def 13;
then reconsider f = x as Function of S,T by A2, WAYBEL10:9;
f is continuous by A2, WAYBEL17:def 2;
hence x in the carrier of (UPS (S,T)) by Def4; :: thesis: verum

end;

then A3: the carrier of (UPS (S,T)) c= the carrier of (MonMaps (S,T)) by YELLOW_0:def 13;
UPS (S,T) is full SubRelStr of T |^ the carrier of S by Def4;
then the InternalRel of (UPS (S,T)) = the InternalRel of (T |^ the carrier of S) |_2 the carrier of (UPS (S,T)) by YELLOW_0:def 14
.= ( the InternalRel of (T |^ the carrier of S) |_2 the carrier of (MonMaps (S,T))) |_2 the carrier of (UPS (S,T)) by A3, WELLORD1:22
.= the InternalRel of (MonMaps (S,T)) |_2 the carrier of (SCMaps (S,T)) by A1, YELLOW_0:def 14
.= the InternalRel of (SCMaps (S,T)) by YELLOW_0:def 14 ;
hence UPS (S,T) = SCMaps (S,T) by A1; :: thesis: verum