let X be non empty TopSpace; :: thesis: for x being Point of X
for D being Subset of X st D is anti-discrete & Cl {x} c= D holds
D = Cl {x}
let x be Point of X; :: thesis: for D being Subset of X st D is anti-discrete & Cl {x} c= D holds
D = Cl {x}
let D be Subset of X; :: thesis: ( D is anti-discrete & Cl {x} c= D implies D = Cl {x} )
assume A1: D is anti-discrete ; :: thesis: ( not Cl {x} c= D or D = Cl {x} )
assume A2: Cl {x} c= D ; :: thesis: D = Cl {x}
D c= Cl {x}

proof

( D misses Cl {x} or D c= Cl {x} ) by A1, Def4;
then ( D /\ (Cl {x}) = {} or D c= Cl {x} ) by XBOOLE_0:def 7;
hence D c= Cl {x} by A2, XBOOLE_1:28; :: thesis: verum

end;

hence D = Cl {x} by A2, XBOOLE_0:def 10; :: thesis: verum