( not 3 is trivial & not 678 is zero ) ;
then 3 -root ((678 |^ (3 * 3)) + 1) is irrational by Th25;
hence 3 -root ((678 |^ 9) + 1) is irrational ; :: thesis: verum