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