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