A3: (2 * 0) + 1 in OddNAT ;
for a being Nat st a in OddNAT holds
ex b being Nat st
( b > a & b in OddNAT )

proof

let a be Nat; :: thesis: ( a in OddNAT implies ex b being Nat st
( b > a & b in OddNAT ) )
assume a in OddNAT ; :: thesis: ex b being Nat st
( b > a & b in OddNAT )
then consider k being Element of NAT such that
A4: a = (2 * k) + 1 ;
take b = a + 2; :: thesis: ( b > a & b in OddNAT )
a + 0 < a + 2 by XREAL_1:8;
hence b > a ; :: thesis: b in OddNAT
b = (2 * (k + 1)) + 1 by A4;
hence b in OddNAT ; :: thesis: verum

end;

hence not OddNAT is finite by A3, Th1; :: thesis: verum