theorem :: MONOID_0:49

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