let a, b, c be odd Nat; :: thesis: ( c - b = 2 & b - a = 2 & not 3 divides a & not 3 divides b implies 3 divides c )
assume that
A1: c - b = 2 and
A2: b - a = 2 ; :: thesis: ( 3 divides a or 3 divides b or 3 divides c )
assume A3: ( not 3 divides a & not 3 divides b ) ; :: thesis: 3 divides c
A4: (b - a) mod 3 = ((b mod 3) - (a mod 3)) mod 3 by INT_6:7;

per cases ( ( a mod 3 = 1 & b mod 3 = 1 ) or ( a mod 3 = 1 & b mod 3 = 2 ) or ( a mod 3 = 2 & b mod 3 = 1 ) or ( a mod 3 = 2 & b mod 3 = 2 ) ) by A3, Lm17;

suppose ( a mod 3 = 1 & b mod 3 = 1 ) ; :: thesis: 3 divides c

hence 3 divides c by A2, A4, NAT_D:24, INT_1:73; :: thesis: verum

end;

suppose ( a mod 3 = 1 & b mod 3 = 2 ) ; :: thesis: 3 divides c

hence 3 divides c by A2, A4, NAT_D:24; :: thesis: verum

end;

suppose that a mod 3 = 2 and
A5: b mod 3 = 1 ; :: thesis: 3 divides c

A6: (c - b) mod 3 = ((c mod 3) - (b mod 3)) mod 3 by INT_6:7;
assume not 3 divides c ; :: thesis: contradiction

per cases then ( c mod 3 = 1 or c mod 3 = 2 ) by Lm17;

suppose c mod 3 = 1 ; :: thesis: contradiction

hence contradiction by A1, A6, A5, NAT_D:24, INT_1:73; :: thesis: verum

end;

suppose c mod 3 = 2 ; :: thesis: contradiction

hence contradiction by A1, A6, A5, NAT_D:24; :: thesis: verum

end;

end;

end;

suppose ( a mod 3 = 2 & b mod 3 = 2 ) ; :: thesis: 3 divides c

hence 3 divides c by A2, A4, INT_1:73; :: thesis: verum

end;

end;