theorem Th1: :: AOFA_A01:1

( 1 mod 2 = 1 & 2 mod 2 = 0 ) by NAT_D:24, NAT_D:25;