theorem Th30: :: FRECHET:30

for A being Subset of R^1
for B being Subset of REAL? st A = B holds
( NAT /\ A = {} & A is open iff ( not REAL in B & B is open ) )