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 )
thus ( A is maximal_discrete implies A is trivial ) by Th38; :: thesis: ( A is trivial implies A is maximal_discrete )
hereby :: thesis: verum
A1: now :: thesis: for D being Subset of X st D is discrete & A c= D holds
A = D
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, Th38;
hence A = D by A3, Th1; :: thesis: verum
end;
assume A is trivial ; :: thesis: A is maximal_discrete
then A is discrete by Th38;
hence A is maximal_discrete by A1; :: thesis: verum
end;