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 A3: D is anti-discrete ; :: thesis: ( not A c= D or A = D )
assume A4: A c= D ; :: thesis: A = D
D c= A

proof

( D misses A or D c= A ) by A2, A3, Def3;
then ( D /\ A = {} or D c= A ) by XBOOLE_0:def 7;
hence D c= A by A4, XBOOLE_1:28; :: thesis: verum

end;

hence A = D by A4, XBOOLE_0:def 10; :: thesis: verum

end;

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