given y being object such that A1: [{},y] in REAL+ ; :: thesis: contradiction

per cases ( [{},y] in RAT+ or [{},y] in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ) by A1, Lm3, XBOOLE_0:def 3;

suppose [{},y] in RAT+ ; :: thesis: contradiction

hence contradiction by ARYTM_3:61; :: thesis: verum

end;

suppose [{},y] in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ; :: thesis: contradiction

hence contradiction by Lm1; :: thesis: verum

end;

end;