set RP = { r where r is Real : 0 <= r } ;
thus REAL+ c= { r where r is Real : 0 <= r } :: according to XBOOLE_0:def 10 :: thesis:

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: e in REAL+ ; :: thesis:
then reconsider r = e as Real by ARYTM_0:1;
reconsider o = 0 , s = r as Element of REAL+ by A1, ARYTM_2:20;
o <=' s by ARYTM_1:6;
then 0 <= r by ARYTM_2:20, XXREAL_0:def 5;
hence e in { r where r is Real : 0 <= r } ; :: thesis:

end;