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