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