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

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

A3: now :: thesis:

let D be Subset of X; :: thesis:
assume A4: D is anti-discrete ; :: thesis:
assume A5: A c= D ; :: thesis:
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:

end;

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

end;

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

A8: now :: thesis:

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

end;

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