let m be Power of n; :: thesis: not m is trivial
consider l being non zero Nat such that
A: m = n |^ l by defpower;
B: 2 <= n by NAT_2:29;
0 + 1 < l + 1 by XREAL_1:6;
then 1 <= l by NAT_1:13;
then n |^ 1 <= n |^ l by NAT_6:1;
then ( m <> 0 & m <> 1 ) by A, B, XXREAL_0:2;
hence not m is trivial by NAT_2:def 1; :: thesis: verum