let X be non empty TopSpace; :: thesis: for Y0 being non empty SubSpace of X
for A being Subset of X st A = the carrier of Y0 holds
( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete )
let Y0 be non empty SubSpace of X; :: thesis: for A being Subset of X st A = the carrier of Y0 holds
( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete )
let A be Subset of X; :: thesis: ( A = the carrier of Y0 implies ( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete ) )
assume A1: A = the carrier of Y0 ; :: thesis: ( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete )
thus ( Y0 is maximal_anti-discrete implies A is maximal_anti-discrete ) :: thesis: ( A is maximal_anti-discrete implies Y0 is maximal_anti-discrete )

proof

assume A2: Y0 is maximal_anti-discrete ; :: thesis: A is maximal_anti-discrete

A3: now :: thesis: for D being Subset of X st D is anti-discrete & A c= D holds
A = D

let D be Subset of X; :: thesis: ( D is anti-discrete & A c= D implies A = D )
assume A4: D is anti-discrete ; :: thesis: ( A c= D implies A = D )
assume A5: A c= D ; :: thesis: A = D
then D <> {} by A1;
then consider X0 being non empty strict SubSpace of X such that
A6: D = the carrier of X0 by TSEP_1:10;
X0 is anti-discrete by A4, A6, Th67;
hence A = D by A1, A2, A5, A6; :: thesis: verum

end;

A is anti-discrete by A1, A2, Th66;
hence A is maximal_anti-discrete by A3; :: thesis: verum

end;

assume A7: A is maximal_anti-discrete ; :: thesis: Y0 is maximal_anti-discrete

A8: now :: thesis: for X0 being SubSpace of X st X0 is anti-discrete & the carrier of Y0 c= the carrier of X0 holds
the carrier of Y0 = the carrier of X0

let X0 be SubSpace of X; :: thesis: ( X0 is anti-discrete & the carrier of Y0 c= the carrier of X0 implies the carrier of Y0 = the carrier of X0 )
reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is anti-discrete ; :: thesis: ( the carrier of Y0 c= the carrier of X0 implies the carrier of Y0 = the carrier of X0 )
then A9: D is anti-discrete by Th66;
assume the carrier of Y0 c= the carrier of X0 ; :: thesis: the carrier of Y0 = the carrier of X0
hence the carrier of Y0 = the carrier of X0 by A1, A7, A9; :: thesis: verum

end;

A is anti-discrete by A7;
then Y0 is anti-discrete by A1, Th67;
hence Y0 is maximal_anti-discrete by A8; :: thesis: verum