let n be Nat; :: thesis: ( ((2 * n) ^2) mod 8 = 0 or ((2 * n) ^2) mod 8 = 4 )
((2 * n) ^2) mod 8 = (4 * (n ^2)) mod 8 ;
hence ( ((2 * n) ^2) mod 8 = 0 or ((2 * n) ^2) mod 8 = 4 ) by NUMBER07:8; :: thesis: verum