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

now :: thesis: contradiction

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

suppose X0 is open ; :: thesis: contradiction

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

end;

suppose X0 is closed ; :: thesis: contradiction

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

end;

end;

end;

hence contradiction ; :: thesis: verum