let X be non empty set ; :: thesis: for x0 being Element of X
for A being non empty Subset of (x0 -PointClTop X) holds Cl A = A \/ {x0}
let x0 be Element of X; :: thesis: for A being non empty Subset of (x0 -PointClTop X) holds Cl A = A \/ {x0}
let A be non empty Subset of (x0 -PointClTop X); :: thesis: Cl A = A \/ {x0}
thus Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) by Def7
.= A \/ ({x0} /\ X) by FUNCOP_1:def 8
.= A \/ {x0} by XBOOLE_1:28 ; :: thesis: verum