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+

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

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 { r where r is Real : 0 <= r } or e in REAL+ )
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;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

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