n - 1 > 2 - 1 by Def1, XREAL_1:9;
hence not n - 1 is trivial by NAT_2:def 1; :: thesis: verum