let e be Element of EvenNAT \ A; :: thesis: e is even

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

suppose EvenNAT \ A = {} ; :: thesis: e is even

hence e is even by SUBSET_1:def 1; :: thesis: verum

end;

suppose EvenNAT \ A <> {} ; :: thesis: e is even

then reconsider e = e as Element of EvenNAT by XBOOLE_0:def 5;
e is even ;
hence e is even ; :: thesis: verum

end;

end;