( number_e in REAL & not number_e in RAT ) by XREAL_0:def 1;
then number_e in REAL \ RAT by XBOOLE_0:def 5;
hence number_e in REAL \ INT by NUMBERS:14, XBOOLE_1:34, TARSKI:def 3; :: thesis: verum