let n be Nat; :: thesis: ( not n is even or n mod 4 = 0 or n mod 4 = 2 )
assume n is even ; :: thesis: ( n mod 4 = 0 or n mod 4 = 2 )
then consider m being Nat such that
A1: n = 2 * m ;
A2: (2 * m) mod (2 * 2) = 2 * (m mod 2) by INT_4:20;
( m mod 2 = 0 or m mod 2 = 1 ) by NAT_D:12;
hence ( n mod 4 = 0 or n mod 4 = 2 ) by A1, A2; :: thesis: verum