let a be Integer; :: thesis: (a |^ 4) mod 8 is trivial Nat
( (a |^ 4) mod 8 = 0 or (a |^ 4) mod 8 = 1 ) by MOQ8;
hence (a |^ 4) mod 8 is trivial Nat by NAT_2:def 1; :: thesis: verum