:: deftheorem defines two_or_more_are_even_among NUMBER14:def 5 :
for a, b, c being Integer holds
( two_or_more_are_even_among a,b,c iff ( ( a is even & b is even & c is odd ) or ( a is even & b is odd & c is even ) or ( a is odd & b is even & c is even ) or ( a is even & b is even & c is even ) ) );