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 D is anti-discrete ; :: thesis: ( not Cl {x} c= D or D = Cl {x} )
then ( D misses Cl {x} or D c= Cl {x} ) ;
then A1: ( D /\ (Cl {x}) = {} or D c= Cl {x} ) ;
assume Cl {x} c= D ; :: thesis: D = Cl {x}
hence D = Cl {x} by A1, XBOOLE_1:28; :: thesis: verum