let X be finite Subset of NAT; :: thesis: not for k being odd Element of NAT holds k in X

per cases ( not X is empty or X is empty ) ;

suppose not X is empty ; :: thesis: not for k being odd Element of NAT holds k in X

then consider n being Element of NAT such that
A1: X c= (Seg n) \/ {0} by Th1;
A2: not (2 * n) + 1 in X

proof

A3: not (2 * n) + 1 in {0} by TARSKI:def 1;
assume (2 * n) + 1 in X ; :: thesis: contradiction
then (2 * n) + 1 in Seg n by A1, 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 odd Element of NAT holds k in X ; :: thesis: contradiction
hence contradiction by A2; :: thesis: verum

end;

suppose X is empty ; :: thesis: not for k being odd Element of NAT holds k in X

hence not for k being odd Element of NAT holds k in X ; :: thesis: verum

end;

end;