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

proof

assume not X0 is proper ; :: thesis: contradiction
then not A is proper ;
then A2: A = the carrier of X ;
X is SubSpace of X by TSEP_1:2;
then TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of X, the topology of X #) by A2, TSEP_1:5;
hence contradiction by A1, Th12; :: thesis: verum

end;

hence X0 is proper ; :: thesis: verum