let X be non empty TopSpace; :: thesis: for S being complete Scott TopLattice holds oContMaps X,S = ContMaps X,S
let S be complete Scott TopLattice; :: thesis: oContMaps X,S = ContMaps X,S
A1: ( Omega S = TopRelStr(# the carrier of S,the InternalRel of S,the topology of S #) & TopStruct(# the carrier of X,the topology of X #) = TopStruct(# the carrier of X,the topology of X #) ) by WAYBEL25:15;
thus oContMaps X,S = ContMaps X,(Omega S) by WAYBEL26:def 1
.= ContMaps X,S by A1, Th13 ; :: thesis: verum