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