let X0 be non empty proper SubSpace of X; :: thesis: ( not X0 is open & not X0 is closed )
reconsider A = the carrier of X0 as non empty Subset of X by Lm1;
set B = A ` ;
X: A is proper by Def3;
then A1: A <> the carrier of X by SUBSET_1:def 7;
A2: ( A ` <> {} & A ` <> the carrier of X ) by X, TOPS_3:1;
assume A3: ( X0 is open or X0 is closed ) ; :: thesis: contradiction

now

per cases ( X0 is open or X0 is closed ) by A3;

suppose X0 is open ; :: thesis: contradiction

then A is open by TSEP_1:def 1;
then A in the topology of X by PRE_TOPC:def 5;
then A in {{} ,the carrier of X} by TDLAT_3:def 2;
hence contradiction by A1, TARSKI:def 2; :: thesis: verum

end;

suppose X0 is closed ; :: thesis: contradiction

then A is closed by BORSUK_1:def 14;
then A ` in the topology of X by PRE_TOPC:def 5;
then A ` in {{} ,the carrier of X} by TDLAT_3:def 2;
hence contradiction by A2, TARSKI:def 2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum