let X0 be SubSpace of X; :: thesis: ( not X0 is proper implies ( X0 is open & X0 is closed ) )
assume not X0 is proper ; :: thesis: ( X0 is open & X0 is closed )
then A1: ex A being Subset of X st
( A = the carrier of X0 & not A is proper ) ;
then A2: for A being Subset of X st A = the carrier of X0 holds
A is closed ;
now :: thesis: for A being Subset of X st A = the carrier of X0 holds
A is open
let A be Subset of X; :: thesis: ( A = the carrier of X0 implies A is open )
assume A = the carrier of X0 ; :: thesis: A is open
then A = [#] X by A1;
hence A is open ; :: thesis: verum
end;
hence ( X0 is open & X0 is closed ) by A2, BORSUK_1:def 11, TSEP_1:def 1; :: thesis: verum