a mod 8 < 7 + 1 by NAT_D:1;
then a mod 8 <= 7 by NAT_1:13;
then not not a mod 8 = 0 & ... & not a mod 8 = 7 ;
then ( (a |^ 2) mod 8 = (0 |^ 2) mod 8 or (a |^ 2) mod 8 = (1 |^ 2) mod 8 or (a |^ 2) mod 8 = (2 |^ 2) mod 8 or (a |^ 2) mod 8 = (3 |^ 2) mod 8 or (a |^ 2) mod 8 = (4 |^ 2) mod 8 or (a |^ 2) mod 8 = (5 |^ 2) mod 8 or (a |^ 2) mod 8 = (6 |^ 2) mod 8 or (a |^ 2) mod 8 = (7 |^ 2) mod 8 ) by GR_CY_3:30;
then A1: ( (a |^ 2) mod 8 = (0 * 0) mod 8 or (a |^ 2) mod 8 = (1 * 1) mod 8 or (a |^ 2) mod 8 = (2 * 2) mod 8 or (a |^ 2) mod 8 = (3 * 3) mod 8 or (a |^ 2) mod 8 = (4 * 4) mod 8 or (a |^ 2) mod 8 = (5 * 5) mod 8 or (a |^ 2) mod 8 = (6 * 6) mod 8 or (a |^ 2) mod 8 = (7 * 7) mod 8 ) by NEWTON:81;
( 1 mod (1 + 7) = (1 * ((8 * 1) + 1)) mod 8 & 1 mod (1 + 7) = (1 * ((8 * 3) + 1)) mod 8 & 1 mod (1 + 7) = (1 * ((8 * 6) + 1)) mod 8 & (4 + (8 * 4)) mod 8 = (4 + ((8 * 4) mod 8)) mod 8 & (0 + (2 * 8)) mod 8 = 0 & (0 + (4 * 8)) mod 8 = 0 ) by NEWTON02:88;
then ( (a |^ 2) mod 8 = 0 mod 8 or (a |^ 2) mod 8 = 1 mod (1 + 7) or (a |^ 2) mod 8 = 4 mod (4 + 4) ) by A1;
then ( (a |^ 2) mod 8 = 0 * 0 or (a |^ 2) mod 8 = 1 * 1 or (a |^ 2) mod 8 = 2 * 2 ) ;
hence (a |^ 2) mod 8 is square ; :: thesis: verum