The abstract of the Mizar article:

Strong Arithmetic of Real Numbers

by

Andrzej Trybulec

Received January 1, 1989

MML identifier: AXIOMS

[ Mizar article, MML identifier index ]

environ

 vocabulary BOOLE, ARYTM, ARYTM_2, ARYTM_3, ORDINAL2, ARYTM_1, ORDINAL1,
      COMPLEX1, OPPCAT_1, RELAT_1, FUNCOP_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL2, FUNCT_4,
      ARYTM_2, ARYTM_1, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0;
 constructors ARYTM_1, ARYTM_0, XREAL_0, XCMPLX_0, FUNCT_4, XBOOLE_0;
 clusters XREAL_0, ARYTM_2, ARYTM_3, ORDINAL2, NUMBERS, XCMPLX_0, ZFMISC_1,
      XBOOLE_0;
 requirements SUBSET, BOOLE, NUMERALS, ARITHM;


begin

reserve x,y,z for real number,
        k for natural number,
        i for Element of NAT;

canceled 18;

theorem :: AXIOMS:19
   ex y st x + y = 0;

theorem :: AXIOMS:20
   x <> 0 implies ex y st x * y = 1;

theorem :: AXIOMS:21
 x <= y & y <= x implies x = y;

theorem :: AXIOMS:22
   x <= y & y <= z implies x <= z;

canceled;

theorem :: AXIOMS:24
   x <= y implies x + z <= y + z;

theorem :: AXIOMS:25
   x <= y & 0 <= z implies x * z <= y * z;

reserve r,r1,r2 for Element of REAL+;

theorem :: AXIOMS:26
   for X,Y being Subset of REAL st for x,y st x in X & y in Y holds x <= y
  ex z st for x,y st x in X & y in Y holds x <= z & z <= y;

canceled;

theorem :: AXIOMS:28
   x in NAT & y in NAT implies x + y in NAT;

theorem :: AXIOMS:29
   for A being Subset of REAL
   st 0 in A & for x st x in A holds x + 1 in A
 holds NAT c= A;

theorem :: AXIOMS:30
   k = { i: i < k };