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 ) by Def3;

A2: now

let A be Subset of X; :: thesis: ( A = the carrier of X0 implies A is closed )
assume A = the carrier of X0 ; :: thesis: A is closed
then A = [#] X by A1, SUBSET_1:def 6;
hence A is closed ; :: thesis: verum

end;

now

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, SUBSET_1:def 6;
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