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;