let X be non empty TopSpace; :: thesis: for x being Point of X st Cl {x} = {x} holds

{x} is maximal_anti-discrete

let x be Point of X; :: thesis: ( Cl {x} = {x} implies {x} is maximal_anti-discrete )

assume A1: Cl {x} = {x} ; :: thesis: {x} is maximal_anti-discrete

{x} is anti-discrete by Th6;

hence {x} is maximal_anti-discrete by A1, Th17; :: thesis: verum

{x} is maximal_anti-discrete

let x be Point of X; :: thesis: ( Cl {x} = {x} implies {x} is maximal_anti-discrete )

assume A1: Cl {x} = {x} ; :: thesis: {x} is maximal_anti-discrete

{x} is anti-discrete by Th6;

hence {x} is maximal_anti-discrete by A1, Th17; :: thesis: verum