theorem lemcontr1: :: FIELD_10:2

for r being Rational holds
( r |^ 3 >= 0 iff r >= 0 )