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