let T be non empty TopSpace; :: thesis: for A being Subset of T st not A is closed holds
for a being Point of T st A \/ {a} is closed holds
Cl A = A \/ {a}
let A be Subset of T; :: thesis: ( not A is closed implies for a being Point of T st A \/ {a} is closed holds
Cl A = A \/ {a} )
assume A1: not A is closed ; :: thesis: for a being Point of T st A \/ {a} is closed holds
Cl A = A \/ {a}
let a be Point of T; :: thesis: ( A \/ {a} is closed implies Cl A = A \/ {a} )
assume A2: A \/ {a} is closed ; :: thesis: Cl A = A \/ {a}
A c= A \/ {a} by XBOOLE_1:7;
then ( A c= Cl A & Cl A c= Cl (A \/ {a}) & Cl (A \/ {a}) = A \/ {a} ) by A2, PRE_TOPC:48, PRE_TOPC:49, PRE_TOPC:52;
hence Cl A = A \/ {a} by A1, BORSUK_5:2; :: thesis: verum