:: REAL_1 semantic presentation begin registration cluster -> real for Element of REAL ; coherence for b1 being Element of REAL holds b1 is real ; end; definition mode Real is Element of REAL ; end; registration clusterV11() ext-real positive real for Element of REAL ; existence ex b1 being Real st b1 is positive proof take 1 ; ::_thesis: 1 is positive thus 1 is positive ; ::_thesis: verum end; end; definition let x be Real; :: original: - redefine func - x -> Real; coherence - x is Real by XREAL_0:def_1; :: original: " redefine funcx " -> Real; coherence x " is Real by XREAL_0:def_1; end; definition let x be real number ; let y be Real; :: original: + redefine funcx + y -> Real; coherence x + y is Real by XREAL_0:def_1; :: original: * redefine funcx * y -> Real; coherence x * y is Real by XREAL_0:def_1; :: original: - redefine funcx - y -> Real; coherence x - y is Real by XREAL_0:def_1; :: original: / redefine funcx / y -> Real; coherence x / y is Real by XREAL_0:def_1; end; definition let x be Real; let y be real number ; :: original: + redefine funcx + y -> Real; coherence x + y is Real by XREAL_0:def_1; :: original: * redefine funcx * y -> Real; coherence x * y is Real by XREAL_0:def_1; :: original: - redefine funcx - y -> Real; coherence x - y is Real by XREAL_0:def_1; :: original: / redefine funcx / y -> Real; coherence x / y is Real by XREAL_0:def_1; end; theorem :: REAL_1:1 REAL+ = { r where r is Real : 0 <= r } proof 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 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 ARYTM_2:20, A1; 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 A2: 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 A2, XXREAL_0:def_5; ::_thesis: verum end;