let X be non empty discrete TopSpace; :: thesis: for A being Subset of X holds
( A is maximal_discrete iff not A is proper )
let A be Subset of X; :: thesis: ( A is maximal_discrete iff not A is proper )

hereby :: thesis: ( not A is proper implies A is maximal_discrete )

X is SubSpace of X by TSEP_1:2;
then reconsider C = the carrier of X as Subset of X by TSEP_1:1;
assume A1: A is maximal_discrete ; :: thesis: not A is proper
C is discrete by Th21;
then A = C by A1;
hence not A is proper ; :: thesis: verum

end;

thus ( not A is proper implies A is maximal_discrete ) by Th21, XBOOLE_0:def 10; :: thesis: verum