reconsider a = a, b = b as odd square Element of NAT by ORDINAL1:def 12;
( 4 divides 2 * 4 & 2 * 4 divides a - b ) by NEWTON03:19;
then 4 divides a - b by INT_2:9;
then not 2 * 2 divides (a |^ 1) + (b |^ 1) by NEWTON03:20;
then not 2 * 2 divides 2 * ((a + b) / 2) ;
hence not (a + b) / 2 is even by INT_4:7; :: thesis: verum