let X be non empty almost_discrete TopSpace; :: thesis: for a, b being Point of X st a in Cl {b} holds
Cl {a} = Cl {b}
let a, b be Point of X; :: thesis: ( a in Cl {b} implies Cl {a} = Cl {b} )
assume a in Cl {b} ; :: thesis: Cl {a} = Cl {b}
then A1: {a} c= Cl {b} by ZFMISC_1:31;
b in Cl {a}
proof
assume not b in Cl {a} ; :: thesis: contradiction
then A2: {b} misses Cl {a} by ZFMISC_1:50;
Cl {a} is open by TDLAT_3:22;
then Cl {b} misses Cl {a} by A2, TSEP_1:36;
then (Cl {b}) /\ (Cl {a}) = {} ;
then Cl {a} = {} by A1, TOPS_1:5, XBOOLE_1:28;
hence contradiction by PRE_TOPC:18, XBOOLE_1:3; :: thesis: verum
end;
then {b} c= Cl {a} by ZFMISC_1:31;
then A3: Cl {b} c= Cl {a} by TOPS_1:5;
Cl {a} c= Cl {b} by A1, TOPS_1:5;
hence Cl {a} = Cl {b} by A3; :: thesis: verum