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 object ; :: according to TARSKI:def 3 :: thesis: ( not e in REAL+ or e in { r where r is Real : 0 <= r } )
assume A1: 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 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: verum

end;

let e be object ; :: 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 A2: ex r being Real st
( e = r & 0 <= r ) ;
not 0 in [:{0},REAL+:] by ARYTM_0:5, ARYTM_2:20, XBOOLE_0:3;
hence e in REAL+ by A2, XXREAL_0:def 5; :: thesis: verum