for x being set holds
( x is Element of <REAL,*> iff x is Element of REAL ) ;