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;