:: deftheorem Def9 defines numberR NUMBER14:def 9 :
for a, b, c being Integer holds
( ( two_or_more_are_even_among a,b,c implies numberR (a,b,c) = 1 ) & ( not two_or_more_are_even_among a,b,c implies numberR (a,b,c) = 0 ) );