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

take Y ; :: thesis: ( Y is strict & Y is closed )

Y is closed

proof

hence
( Y is strict & Y is closed )
; :: thesis: verum
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;assume A = the carrier of Y ; :: thesis: A is closed

then A = [#] X ;

hence A is closed ; :: thesis: verum