let X0 be non empty SubSpace of X; :: thesis: ( X0 is maximal_discrete implies X0 is proper )
assume A1: X0 is maximal_discrete ; :: thesis: X0 is proper
reconsider A = the carrier of X0 as Subset of X by Lm1;
A is maximal_discrete by A1, Def8;
then A is discrete by Def7;
then A2: X0 is discrete by Th26;
X0 is proper

proof

assume not X0 is proper ; :: thesis: contradiction
then not A is proper by Th13;
then ( A = the carrier of X & X is SubSpace of X ) by SUBSET_1:def 7, TSEP_1:2;
then TopStruct(# the carrier of X0,the topology of X0 #) = TopStruct(# the carrier of X,the topology of X #) by TSEP_1:5;
hence contradiction by A2, Th17; :: thesis: verum

end;

hence X0 is proper ; :: thesis: verum