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 )

assume A1: A is maximal_discrete ; :: thesis: not A is proper
X is SubSpace of X by TSEP_1:2;
then reconsider C = the carrier of X as Subset of X by TSEP_1:1;
( C is discrete & A c= C ) by Th27;
then A = C by A1, Def7;
hence not A is proper by SUBSET_1:def 7; :: thesis: verum

end;

hereby :: thesis: verum

assume not A is proper ; :: thesis: A is maximal_discrete
then A2: A = the carrier of X by SUBSET_1:def 7;
then A3: A is discrete by Th27;
for D being Subset of X st D is discrete & A c= D holds
A = D by A2, XBOOLE_0:def 10;
hence A is maximal_discrete by A3, Def7; :: thesis: verum

end;