let S, T be complete Scott TopLattice; :: thesis: SCMaps S,T = ContMaps S,T
reconsider Sm = ContMaps S,T as non empty full SubRelStr of T |^ the carrier of S by Def3;
reconsider SC = SCMaps S,T as non empty full SubRelStr of T |^ the carrier of S by WAYBEL15:1;
A1: the carrier of SC c= the carrier of (MonMaps S,T) by YELLOW_0:def 13;
A2: the carrier of SC c= the carrier of Sm

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of SC or a in the carrier of Sm )
assume A3: a in the carrier of SC ; :: thesis: a in the carrier of Sm
then reconsider f = a as Function of S,T by A1, WAYBEL10:10;
f is continuous Function of S,T by A3, WAYBEL17:def 2;
then a is Element of Sm by Th21;
hence a in the carrier of Sm ; :: thesis: verum

end;

the carrier of Sm c= the carrier of SC

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of Sm or a in the carrier of SC )
assume a in the carrier of Sm ; :: thesis: a in the carrier of SC
then a is continuous Function of S,T by Th21;
hence a in the carrier of SC by WAYBEL17:def 2; :: thesis: verum

end;

then the carrier of SC = the carrier of Sm by A2, XBOOLE_0:def 10;
hence SCMaps S,T = ContMaps S,T by YELLOW_0:58; :: thesis: verum