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