A1: 2 * 0 in EvenNAT ;
for a being Nat st a in EvenNAT holds
ex b being Nat st
( b > a & b in EvenNAT )

proof

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

end;

hence not EvenNAT is finite by A1, Th1; :: thesis: verum