theorem Th29: :: FRECHET:29

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