theorem Th1: :: FDIFF_1:1

for Y being Subset of REAL holds
( ( for r being Real holds
( r in Y iff r in REAL ) ) iff Y = REAL )