let X be non empty set ; :: thesis: for x0 being Element of X

for A being non empty Subset of (x0 -PointClTop X) holds

( A is closed iff x0 in A )

let x0 be Element of X; :: thesis: for A being non empty Subset of (x0 -PointClTop X) holds

( A is closed iff x0 in A )

let A be non empty Subset of (x0 -PointClTop X); :: thesis: ( A is closed iff x0 in A )

( A is closed iff Cl A = A ) by PRE_TOPC:22;

then ( A is closed iff A = A \/ {x0} ) by Th37;

then ( A is closed iff {x0} c= A ) by XBOOLE_1:7, XBOOLE_1:12;

hence ( A is closed iff x0 in A ) by ZFMISC_1:31; :: thesis: verum

for A being non empty Subset of (x0 -PointClTop X) holds

( A is closed iff x0 in A )

let x0 be Element of X; :: thesis: for A being non empty Subset of (x0 -PointClTop X) holds

( A is closed iff x0 in A )

let A be non empty Subset of (x0 -PointClTop X); :: thesis: ( A is closed iff x0 in A )

( A is closed iff Cl A = A ) by PRE_TOPC:22;

then ( A is closed iff A = A \/ {x0} ) by Th37;

then ( A is closed iff {x0} c= A ) by XBOOLE_1:7, XBOOLE_1:12;

hence ( A is closed iff x0 in A ) by ZFMISC_1:31; :: thesis: verum