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 Th14;
then {x} c= D by A3, XBOOLE_1:1;
then x in D by ZFMISC_1:31;
then D c= MaxADSet x by A2, Th21;
hence MaxADSet x = D by A3, XBOOLE_0:def 10; :: thesis: verum

end;

MaxADSet x is anti-discrete by Th15;
hence MaxADSet x is maximal_anti-discrete by A1, Def7; :: thesis: verum