theorem lemcontr: :: FIELD_10:3

for r being Rational holds not r |^ 3 = 2