environ
vocabularies HIDDEN, ARYTM_2, SUBSET_1, ARYTM_3, ZFMISC_1, CARD_1, XXREAL_0, NUMBERS, ARYTM_0, FUNCOP_1, XBOOLE_0, TARSKI, NAT_1, REAL_1, ORDINAL1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FUNCT_4, ARYTM_2, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, XXREAL_0;
definitions TARSKI, XBOOLE_0, XXREAL_0;
theorems XBOOLE_0, ARYTM_0, ZFMISC_1, TARSKI, ARYTM_1, ARYTM_2, SUBSET_1, ORDINAL1, XBOOLE_1, XREAL_0, XCMPLX_0, NUMBERS, XXREAL_0, XTUPLE_0;
schemes ;
registrations ORDINAL1, ARYTM_2, XREAL_0;
constructors HIDDEN, FUNCT_4, ARYTM_1, ARYTM_0, XCMPLX_0, XXREAL_0, XREAL_0;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, ARITHM;
equalities XBOOLE_0, ARYTM_3, ORDINAL1;
expansions TARSKI;
Lm1:
for r, s being Real st ( ( r in REAL+ & s in REAL+ & ex x9, y9 being Element of REAL+ st
( r = x9 & s = y9 & x9 <=' y9 ) ) or ( r in [:{0},REAL+:] & s in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( r = [0,x9] & s = [0,y9] & y9 <=' x9 ) ) or ( s in REAL+ & r in [:{0},REAL+:] ) ) holds
r <= s
Lm2:
for x being Real
for x1, x2 being Element of REAL st x = [*x1,x2*] holds
( x2 = 0 & x = x1 )
Lm3:
for x9, y9 being Element of REAL
for x, y being Real st x9 = x & y9 = y holds
+ (x9,y9) = x + y
Lm4:
{} in {{}}
by TARSKI:def 1;
reconsider o = 0 as Element of REAL+ by ARYTM_2:20;