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

hereby :: thesis: ( A is trivial implies A is maximal_discrete )

assume A is maximal_discrete ; :: thesis: A is trivial
then A is discrete by Def7;
hence A is trivial by Th44; :: thesis: verum

end;

hereby :: thesis: verum

A1: now

let D be Subset of X; :: thesis: ( D is discrete & A c= D implies A = D )
assume A2: D is discrete ; :: thesis: ( A c= D implies A = D )
assume A3: A c= D ; :: thesis: A = D
then reconsider E = D as non empty Subset of X ;
E is trivial by A2, Th44;
hence A = D by A3, Th1; :: thesis: verum

end;

assume A is trivial ; :: thesis: A is maximal_discrete
then A is discrete by Th44;
hence A is maximal_discrete by A1, Def7; :: thesis: verum

end;