InclPoset the topology of X, oContMaps X,Sierpinski_Space are_isomorphic by WAYBEL26:6;
hence oContMaps X,Sierpinski_Space is complete by WAYBEL20:18; :: thesis: verum