let e be Element of EvenNAT ; :: thesis: e is even
e in EvenNAT ;
hence e is even ; :: thesis: verum