let Y be non empty TopStruct ; :: thesis: for A being non empty Subset of Y st A is anti-discrete & A is open holds
A is maximal_anti-discrete
let A be non empty Subset of Y; :: thesis: ( A is anti-discrete & A is open implies A is maximal_anti-discrete )
assume A1: A is anti-discrete ; :: thesis: ( not A is open or A is maximal_anti-discrete )
assume A2: A is open ; :: thesis: A is maximal_anti-discrete
for D being Subset of Y st D is anti-discrete & A c= D holds
A = D

proof

let D be Subset of Y; :: thesis: ( D is anti-discrete & A c= D implies A = D )
assume D is anti-discrete ; :: thesis: ( not A c= D or A = D )
then ( D misses A or D c= A ) by A2;
then A3: ( D /\ A = {} or D c= A ) ;
assume A c= D ; :: thesis: A = D
hence A = D by A3, XBOOLE_1:28; :: thesis: verum

end;

hence A is maximal_anti-discrete by A1; :: thesis: verum