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 consider A being Subset of X such that
A1: A = the carrier of X0 and
A2: not A is proper by Def3;

A3: 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, A2, SUBSET_1:def 7;
hence A is open ; :: thesis: verum

end;

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, A2, SUBSET_1:def 7;
hence A is closed ; :: thesis: verum

end;

hence ( X0 is open & X0 is closed ) by A3, BORSUK_1:def 14, TSEP_1:def 1; :: thesis: verum