(3 -Root 2) |^ 3 = 2 by PREPOWER:def 2;
hence not 3 -Root 2 is rational by lemcontr; :: thesis: verum