let Y be non empty TopStruct ; :: thesis: for x being Point of Y holds MaxADSet x is maximal_anti-discrete
let x be Point of Y; :: thesis: MaxADSet x is maximal_anti-discrete
A1: for D being Subset of Y st D is anti-discrete & MaxADSet x c= D holds
MaxADSet x = D

proof

let D be Subset of Y; :: thesis: ( D is anti-discrete & MaxADSet x c= D implies MaxADSet x = D )
assume A2: D is anti-discrete ; :: thesis: ( not MaxADSet x c= D or MaxADSet x = D )
assume A3: MaxADSet x c= D ; :: thesis: MaxADSet x = D
{x} c= MaxADSet x by Th12;
then {x} c= D by A3;
then x in D by ZFMISC_1:31;
then D c= MaxADSet x by A2, Th19;
hence MaxADSet x = D by A3; :: thesis: verum

end;

MaxADSet x is anti-discrete by Th13;
hence MaxADSet x is maximal_anti-discrete by A1; :: thesis: verum