:: deftheorem Def10 defines numberR0 NUMBER14:def 10 :
for a, b, c being Integer holds
( ( a,b,c give_three_different_remainders_upon_dividing_by 3 implies numberR0 (a,b,c) = 0 ) & ( ( a mod 3 = b mod 3 or a mod 3 = c mod 3 ) implies numberR0 (a,b,c) = 1 - (a mod 3) ) & ( a,b,c give_three_different_remainders_upon_dividing_by 3 or a mod 3 = b mod 3 or a mod 3 = c mod 3 or numberR0 (a,b,c) = 1 - (b mod 3) ) );