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

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

( A is open iff not x0 in A )

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

( A is open iff not x0 in A )

let A be proper Subset of (x0 -PointClTop X); :: thesis: ( A is open iff not x0 in A )

( A is open iff A ` is closed ) by TOPS_1:4;

then A1: ( A is open iff x0 in A ` ) by Th38;

x0 is Element of (x0 -PointClTop X) by Def7;

hence ( A is open iff not x0 in A ) by A1, XBOOLE_0:def 5; :: thesis: verum

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

( A is open iff not x0 in A )

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

( A is open iff not x0 in A )

let A be proper Subset of (x0 -PointClTop X); :: thesis: ( A is open iff not x0 in A )

( A is open iff A ` is closed ) by TOPS_1:4;

then A1: ( A is open iff x0 in A ` ) by Th38;

x0 is Element of (x0 -PointClTop X) by Def7;

hence ( A is open iff not x0 in A ) by A1, XBOOLE_0:def 5; :: thesis: verum