now :: thesis: for m being Nat ex n being Nat st
( n >= m & n in EvenNAT )

let m be Nat; :: thesis: ex n being Nat st
( n >= m & n in EvenNAT )
reconsider n = 2 * m as Nat ;

now :: thesis: ( n >= m & n in EvenNAT )

1 * m <= 2 * m by NAT_1:4;
hence n >= m ; :: thesis: n in EvenNAT
thus n in EvenNAT by FIB_NUM2:def 3; :: thesis: verum

end;

hence ex n being Nat st
( n >= m & n in EvenNAT ) ; :: thesis: verum

end;

then EvenNAT is infinite by PYTHTRIP:9;
hence EvenNAT is denumerable ; :: thesis: verum