let X, Y be non empty TopSpace; :: thesis: the carrier of (oContMaps X,Y) c= Funcs the carrier of X,the carrier of Y
oContMaps X,Y is SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def 3;
then the carrier of (oContMaps X,Y) c= the carrier of ((Omega Y) |^ the carrier of X) by YELLOW_0:def 13;
then ( the carrier of (oContMaps X,Y) c= Funcs the carrier of X,the carrier of (Omega Y) & TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of (Omega Y),the topology of (Omega Y) #) ) by WAYBEL25:def 2, YELLOW_1:28;
hence the carrier of (oContMaps X,Y) c= Funcs the carrier of X,the carrier of Y ; :: thesis: verum