let X be non empty TopSpace; :: thesis: for x being Point of X holds x in Cl {x}
let x be Point of X; :: thesis: x in Cl {x}
( x in {x} & {x} c= Cl {x} ) by PRE_TOPC:18, TARSKI:def 1;
hence x in Cl {x} ; :: thesis: verum