let k be Element of NAT ; :: thesis: ( ( ex j being Element of NAT st k = (2 * j) + 1 implies ( k <> 0 & ( for j being Element of NAT holds not k = (2 * j) + 2 ) ) ) & ( ex j being Element of NAT st k = (2 * j) + 2 implies ( k <> 0 & ( for j being Element of NAT holds not k = (2 * j) + 1 ) ) ) )
thus ( ex j being Element of NAT st k = (2 * j) + 1 implies ( k <> 0 & ( for j being Element of NAT holds not k = (2 * j) + 2 ) ) ) :: thesis: ( ex j being Element of NAT st k = (2 * j) + 2 implies ( k <> 0 & ( for j being Element of NAT holds not k = (2 * j) + 1 ) ) )

proof

given j being Element of NAT such that A1: k = (2 * j) + 1 ; :: thesis: ( k <> 0 & ( for j being Element of NAT holds not k = (2 * j) + 2 ) )
thus k <> 0 by A1; :: thesis: for j being Element of NAT holds not k = (2 * j) + 2
given i being Element of NAT such that A2: k = (2 * i) + 2 ; :: thesis: contradiction
A3: (2 * i) + (2 * 1) = (2 * (i + 1)) + 0 ;
1 = ((2 * i) + 2) mod 2 by A1, A2, NAT_D:def 2
.= 0 by A3, NAT_D:def 2 ;
hence contradiction ; :: thesis: verum

end;

thus ( ex j being Element of NAT st k = (2 * j) + 2 implies ( k <> 0 & ( for j being Element of NAT holds not k = (2 * j) + 1 ) ) ) :: thesis: verum

proof

given j being Element of NAT such that A4: k = (2 * j) + 2 ; :: thesis: ( k <> 0 & ( for j being Element of NAT holds not k = (2 * j) + 1 ) )
thus k <> 0 by A4; :: thesis: for j being Element of NAT holds not k = (2 * j) + 1
given i being Element of NAT such that A5: k = (2 * i) + 1 ; :: thesis: contradiction
A6: (2 * j) + (2 * 1) = (2 * (j + 1)) + 0 ;
1 = ((2 * j) + 2) mod 2 by A4, A5, NAT_D:def 2
.= 0 by A6, NAT_D:def 2 ;
hence contradiction ; :: thesis: verum

end;