let X be non empty TopSpace; :: thesis: InclPoset the topology of X, oContMaps X,Sierpinski_Space are_isomorphic
consider f being Function of (InclPoset the topology of X),(oContMaps X,Sierpinski_Space ) such that
A1: f is isomorphic and
for V being open Subset of X holds f . V = chi V,the carrier of X by Th5;
take f ; :: according to WAYBEL_1:def 8 :: thesis: f is isomorphic
thus f is isomorphic by A1; :: thesis: verum