let s be square Integer; :: thesis: s mod 3 is trivial Nat
2 -root s is integer ;
then reconsider a = 2 -root s as integer number ;
( a |^ 2, 0 are_congruent_mod 3 or a |^ 2,1 are_congruent_mod 3 ) by NAT_6:15;
then ( (a |^ 2) mod 3 = 0 mod 3 or (a |^ 2) mod 3 = 1 mod (1 + 2) ) by NAT_D:64;
hence s mod 3 is trivial Nat by NAT_2:def 1; :: thesis: verum