per cases ( EvenNAT \ A = {} or EvenNAT \ A <> {} ) ;

suppose EvenNAT \ A = {} ; :: thesis: ex b₁ being Element of EvenNAT \ A st b₁ is even

then reconsider e = 0 as Element of EvenNAT \ A by SUBSET_1:def 1;
take e ; :: thesis: e is even
thus e is even ; :: thesis: verum

end;

suppose EvenNAT \ A <> {} ; :: thesis: ex b₁ being Element of EvenNAT \ A st b₁ is even

then consider e being object such that
A1: e in EvenNAT \ A by XBOOLE_0:7;
reconsider e = e as Element of EvenNAT \ A by A1;
take e ; :: thesis: e is even
thus e is even ; :: thesis: verum

end;

end;