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}
A2: A c= Cl A by PRE_TOPC:18;
let a be Point of T; :: thesis: ( A \/ {a} is closed implies Cl A = A \/ {a} )
assume A \/ {a} is closed ; :: thesis: Cl A = A \/ {a}
then A3: Cl (A \/ {a}) = A \/ {a} by PRE_TOPC:22;
Cl A c= Cl (A \/ {a}) by PRE_TOPC:19, XBOOLE_1:7;
hence Cl A = A \/ {a} by A1, A2, A3, ZFMISC_1:138; :: thesis: verum