theorem :: MONOID_0:38

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