let n be Nat; :: thesis: ( not n is odd or n mod 4 = 1 or n mod 4 = 3 )
assume n is odd ; :: thesis: ( n mod 4 = 1 or n mod 4 = 3 )
then consider m being Nat such that
A1: n = (2 * m) + 1 by ABIAN:9;
((2 * m) + 1) mod 4 = (((2 * m) mod 4) + (1 mod 4)) mod 4 by NAT_D:66
.= (((2 * m) mod 4) + 1) mod 4 by NAT_D:24 ;
then ( n mod 4 = (0 + 1) mod 4 or n mod 4 = (2 + 1) mod 4 ) by A1, Th78;
hence ( n mod 4 = 1 or n mod 4 = 3 ) by NAT_D:24; :: thesis: verum