reconsider Y = TopStruct(# the carrier of X, the topology of X #) as strict SubSpace of X by Lm4;
take Y ; :: thesis: ( Y is strict & Y is open )
Y is open

proof

let A be Subset of X; :: according to TSEP_1:def 1 :: thesis: ( A = the carrier of Y implies A is open )
assume A = the carrier of Y ; :: thesis: A is open
then A = [#] X ;
hence A is open ; :: thesis: verum

end;

hence ( Y is strict & Y is open ) ; :: thesis: verum