let a, b, c, r0 be Integer; :: thesis:
assume A1: r0 = numberR0 (a,b,c) ; :: thesis:

per cases ;

suppose A2: a,b,c give_three_different_remainders_upon_dividing_by 3 ; :: thesis:

then A3: a mod 3,b mod 3,c mod 3 are_mutually_distinct ;
A4: r0 = 0 by A1, A2, Def10;
assume ( 3 divides a + r0 or 3 divides b + r0 or not 3 divides c + r0 ) ; :: according to NUMBER14:def 8 :: thesis:
hence ( ( not 3 divides a + r0 & 3 divides b + r0 & not 3 divides c + r0 ) or ( 3 divides a + r0 & not 3 divides b + r0 & not 3 divides c + r0 ) or ( not 3 divides a + r0 & not 3 divides b + r0 & not 3 divides c + r0 ) ) by A3, A4; :: thesis:

end;

suppose A5: not a,b,c give_three_different_remainders_upon_dividing_by 3 ; :: thesis:

then A6: not a mod 3,b mod 3,c mod 3 are_mutually_distinct ;
assume A7: not a + r0,b + r0,c + r0 at_least_two_are_not_divisible_by 3 ; :: thesis:
then A8: ( ( 3 divides a + r0 or 3 divides b + r0 or not 3 divides c + r0 ) & ( 3 divides a + r0 or not 3 divides b + r0 or 3 divides c + r0 ) & ( not 3 divides a + r0 or 3 divides b + r0 or 3 divides c + r0 ) & ( 3 divides a + r0 or 3 divides b + r0 or 3 divides c + r0 ) ) ;
A9: (a + r0) mod 3 = ((a mod 3) + (r0 mod 3)) mod 3 by NAT_D:66;
A10: (b + r0) mod 3 = ((b mod 3) + (r0 mod 3)) mod 3 by NAT_D:66;
A11: (c + r0) mod 3 = ((c mod 3) + (r0 mod 3)) mod 3 by NAT_D:66;
reconsider a3 = a mod 3 as Element of NAT by INT_1:3, INT_1:57;
a mod 3 < 2 + 1 by INT_1:58;
then a3 <= 2 by NAT_1:13;
then A12: not not a3 = 0 & ... & not a3 = 2 ;

per cases by A6;

suppose A13: a mod 3 = b mod 3 ; :: thesis:

then A14: r0 = 1 - (a mod 3) by A1, Def10;

per cases by A12;

suppose r0 = 1 ; :: thesis:

hence contradiction by A7, A9, A10, A13, A14, Lm5, INT_1:62; :: thesis:

end;

suppose r0 = 0 ; :: thesis:

hence contradiction by A8, A13, A14; :: thesis:

end;

suppose r0 = - 1 ; :: thesis:

hence contradiction by A7, A9, A10, A13, A14, Lm5, Lm6, INT_1:62, NUMBER02:9; :: thesis:

end;

end;

end;

suppose A15: a mod 3 = c mod 3 ; :: thesis:

then A16: r0 = 1 - (a mod 3) by A1, Def10;

per cases by A12;

suppose r0 = 1 ; :: thesis:

hence contradiction by A7, A9, A11, A15, A16, Lm5, INT_1:62; :: thesis:

end;

suppose r0 = 0 ; :: thesis:

hence contradiction by A8, A15, A16; :: thesis:

end;

suppose r0 = - 1 ; :: thesis:

hence contradiction by A7, A9, A11, A15, A16, Lm5, Lm6, INT_1:62, NUMBER02:9; :: thesis:

end;

end;

end;

suppose that A17: b mod 3 = c mod 3 and
A18: ( a mod 3 <> b mod 3 & a mod 3 <> c mod 3 ) ; :: thesis:

reconsider b3 = b mod 3 as Element of NAT by INT_1:3, INT_1:57;
b mod 3 < 2 + 1 by INT_1:58;
then b3 <= 2 by NAT_1:13;
then A19: not not b3 = 0 & ... & not b3 = 2 ;
A20: r0 = 1 - (b mod 3) by A1, A5, A18, Def10;

per cases by A19;

suppose r0 = 1 ; :: thesis:

hence contradiction by A7, A10, A11, A17, A20, Lm5, INT_1:62; :: thesis:

end;

suppose r0 = 0 ; :: thesis:

hence contradiction by A8, A17, A20; :: thesis:

end;

suppose r0 = - 1 ; :: thesis:

hence contradiction by A7, A10, A11, A17, A20, Lm5, Lm6, INT_1:62, NUMBER02:9; :: thesis:

end;

end;

end;

end;

end;

end;