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

Sspace x is maximal_anti-discrete

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

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

then A1: {x} is maximal_anti-discrete by Th45;

the carrier of (Sspace x) = {x} by TEX_2:def 2;

hence Sspace x is maximal_anti-discrete by A1, Th72; :: thesis: verum

Sspace x is maximal_anti-discrete

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

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

then A1: {x} is maximal_anti-discrete by Th45;

the carrier of (Sspace x) = {x} by TEX_2:def 2;

hence Sspace x is maximal_anti-discrete by A1, Th72; :: thesis: verum