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)
let x be
set ;
:: 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:10;
f is
continuous
by A2, WAYBEL17:def 2;
then
f is
directed-sups-preserving
;
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:29
.=
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