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