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

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