let m be Element of NAT ; :: thesis: for X being non empty finite Subset of [:NAT,{m}:] holds
not for k being non zero Element of NAT holds [((2 * k) + 1),m] in X
let X be non empty finite Subset of [:NAT,{m}:]; :: thesis: not for k being non zero Element of NAT holds [((2 * k) + 1),m] in X
consider n being non zero Element of NAT such that
A1: X c= [:((Seg n) \/ {0}),{m}:] by Th3;
A2: not [((2 * n) + 1),m] in X

proof

assume [((2 * n) + 1),m] in X ; :: thesis: contradiction
then A3: (2 * n) + 1 in (Seg n) \/ {0} by A1, ZFMISC_1:87;
not (2 * n) + 1 in {0} by TARSKI:def 1;
then (2 * n) + 1 in Seg n by A3, XBOOLE_0:def 3;
then A4: (2 * n) + 1 <= n by FINSEQ_1:1;
1 * n <= 2 * n by NAT_1:4;
hence contradiction by A4, NAT_1:13; :: thesis: verum

end;

assume for k being non zero Element of NAT holds [((2 * k) + 1),m] in X ; :: thesis: contradiction
hence contradiction by A2; :: thesis: verum