let X be non empty set ; :: thesis: for X0 being set

for A being proper Subset of (X0 -DiscreteTop X) holds

( A is open iff A c= X0 )

let X0 be set ; :: thesis: for A being proper Subset of (X0 -DiscreteTop X) holds

( A is open iff A c= X0 )

let A be proper Subset of (X0 -DiscreteTop X); :: thesis: ( A is open iff A c= X0 )

( A is open iff Int A = A ) by TOPS_1:23;

then ( A is open iff A = A /\ X0 ) by Th42;

hence ( A is open iff A c= X0 ) by XBOOLE_1:17, XBOOLE_1:28; :: thesis: verum

for A being proper Subset of (X0 -DiscreteTop X) holds

( A is open iff A c= X0 )

let X0 be set ; :: thesis: for A being proper Subset of (X0 -DiscreteTop X) holds

( A is open iff A c= X0 )

let A be proper Subset of (X0 -DiscreteTop X); :: thesis: ( A is open iff A c= X0 )

( A is open iff Int A = A ) by TOPS_1:23;

then ( A is open iff A = A /\ X0 ) by Th42;

hence ( A is open iff A c= X0 ) by XBOOLE_1:17, XBOOLE_1:28; :: thesis: verum