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

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