given y being set 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:68; :: 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;