for r being object holds
( r in REAL+ \ {0} iff r is positive Real )