let a be Nat; :: thesis: ( ( 3 divides a & not a mod 3 <> 0 ) or a mod 3 = 1 or a mod 3 = 2 )
a mod 3 < 2 + 1 by INT_1:58;
then a mod 3 <= 2 by NAT_1:13;
then not not a mod 3 = 0 & ... & not a mod 3 = 2 ;
hence ( ( 3 divides a & not a mod 3 <> 0 ) or a mod 3 = 1 or a mod 3 = 2 ) by INT_1:62; :: thesis: verum