let a, b be odd Integer; :: thesis: ( (a + b) mod 4 = 2 or (a - b) mod 4 = 2 )
A1: ( (a + b) mod (2 * 2) is even & (a - b) mod (2 * 2) is even ) ;
A2: ( not not (a + b) mod (3 + 1) = 0 & ... & not (a + b) mod (3 + 1) = 3 & not not (a - b) mod (3 + 1) = 0 & ... & not (a - b) mod (3 + 1) = 3 ) by NUMBER03:11;

per cases ( (a + b) mod 4 = 0 or (a + b) mod 4 = 2 ) by A1, A2;

suppose (a + b) mod 4 = 0 ; :: thesis: ( (a + b) mod 4 = 2 or (a - b) mod 4 = 2 )

then 4 divides a + b by INT_1:62;
then not 4 divides a - b by NEWTON03:73;
hence ( (a + b) mod 4 = 2 or (a - b) mod 4 = 2 ) by A1, A2, INT_1:62; :: thesis: verum

end;

suppose (a + b) mod 4 = 2 ; :: thesis: ( (a + b) mod 4 = 2 or (a - b) mod 4 = 2 )

hence ( (a + b) mod 4 = 2 or (a - b) mod 4 = 2 ) ; :: thesis: verum

end;

end;