let X0 be SubSpace of X; :: thesis: ( X0 is closed implies X0 is open )
assume A2: X0 is closed ; :: thesis: X0 is open
let A be Subset of X; :: according to TSEP_1:def 1 :: thesis: ( not A = the carrier of X0 or A is open )
assume A = the carrier of X0 ; :: thesis: A is open
then A is closed by A2, BORSUK_1:def 14;
hence A is open by Th24; :: thesis: verum