reconsider Y = TopStruct(# the carrier of X, the topology of X #) as strict SubSpace of X by Lm2;
take Y ; :: thesis: ( Y is strict & Y is closed )
Y is closed
proof
let A be Subset of X; :: according to BORSUK_1:def 11 :: thesis: ( A = the carrier of Y implies A is closed )
assume A = the carrier of Y ; :: thesis: A is closed
then A = [#] X ;
hence A is closed ; :: thesis: verum
end;
hence ( Y is strict & Y is closed ) ; :: thesis: verum