:: deftheorem Def1 defines ext-real XXREAL_0:def 1 :
for x being object holds
( x is ext-real iff x in ExtREAL );