let n be Nat; :: thesis: ( not n is odd or n,1 are_congruent_mod 4 or n,3 are_congruent_mod 4 )
assume n is odd ; :: thesis: ( n,1 are_congruent_mod 4 or n,3 are_congruent_mod 4 )
then ( n mod 4 = 1 or n mod 4 = 3 ) by Th80;
then ( n mod 4 = 1 mod 4 or n mod 4 = 3 mod 4 ) ;
hence ( n,1 are_congruent_mod 4 or n,3 are_congruent_mod 4 ) by NAT_D:64; :: thesis: verum