:: deftheorem Def1 defines real XREAL_0:def 1 :
for r being object holds
( r is real iff r in REAL );