:: Strong arithmetic of real numbers
:: by Andrzej Trybulec
::
:: Received January 1, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

Lm1:  for r, s being real number st ( ( r in REAL+ & s in REAL+ & ex x9, y9 being Element of REAL+ st
( r = x9 &amp; s = y9 &amp; x9 <=' y9 ) ) or ( r in [:{0},REAL+:] &amp; s in [:{0},REAL+:] &amp; ex x9, y9 being Element of REAL+ st
( r = [0,x9] &amp; s = [0,y9] &amp; y9 <=' x9 ) ) or ( s in REAL+ &amp; r in [:{0},REAL+:] ) ) holds
r <= s
proofend;

Lm2:  for x being real number
for x1, x2 being Element of REAL st x = [*x1,x2*] holds
( x2 = 0 &amp; x = x1 )
proofend;

Lm3:  for x9, y9 being Element of REAL
for x, y being real number st x9 = x &amp; y9 = y holds
+ (x9,y9) = x + y
proofend;

Lm4:  {} in {{}}
by TARSKI:def_1;

reconsider o = 0 as Element of REAL+ by ARYTM_2:20;

theorem :: AXIOMS:1
for X, Y being Subset of REAL st ( for x, y being real number st x in X &amp; y in Y holds
x <= y ) holds
ex z being real number st
for x, y being real number st x in X &amp; y in Y holds
( x <= z &amp; z <= y )
proofend;

theorem :: AXIOMS:2
for x, y being real number st x in NAT &amp; y in NAT holds
x + y in NAT
proofend;

theorem :: AXIOMS:3
for A being Subset of REAL st 0 in A &amp; ( for x being real number st x in A holds
x + 1 in A ) holds
NAT c= A
proofend;

theorem :: AXIOMS:4
for k being Nat holds k =  {  i where i is Element of NAT : i < k  }
proofend;