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: { r where r is Real : 0 <= r } c= REAL+

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in REAL+ or e in { r where r is Real : 0 <= r } )
assume Z: e in REAL+ ; :: thesis: e in { r where r is Real : 0 <= r }
then reconsider r = e as Real by ARYTM_0:1;
reconsider o = 0 , s = r as Element of REAL+ by ARYTM_2:20, Z;
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: verum

end;

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { r where r is Real : 0 <= r } or e in REAL+ )
assume e in { r where r is Real : 0 <= r } ; :: thesis: e in REAL+
then A: ex r being Real st
( e = r & 0 <= r ) ;
not 0 in [:{0},REAL+:] by ARYTM_0:5, XBOOLE_0:3, ARYTM_2:20;
hence e in REAL+ by A, XXREAL_0:def 5; :: thesis: verum