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 by Def8;
then A is discrete by Def7;
then A1: X0 is discrete by Th26;
X0 is proper

proof

assume not X0 is proper ; :: thesis: contradiction
then not A is proper by Th13;
then A2: A = the carrier of X by SUBSET_1:def 6;
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, Th17; :: thesis: verum

end;

hence X0 is proper ; :: thesis: verum