let t be Integer; :: thesis: ( t mod 3 = 0 or t mod 3 = 1 or t mod 3 = 2 )
A1: t mod 3 in NAT by INT_1:3, INT_1:57;
(t mod 3) mod 3 = t mod 3 ;
then t mod 3 < 2 + 1 by A1, NAT_D:1;
hence ( t mod 3 = 0 or t mod 3 = 1 or t mod 3 = 2 ) by A1, NAT_1:22, NAT_1:23; :: thesis: verum