The abstract of the Mizar article:

Preliminaries to Arithmetic

by

Library Committee

Received December 10, 1995

MML identifier: ARYTM

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM_2, BOOLE, ARYTM_1, ARYTM_3, ORDINAL2, ARYTM;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL2, ARYTM_2, ARYTM_1,
      ARYTM_0;
 constructors ARYTM_1, ARYTM_0;
 clusters ARYTM_2, ARYTM_0;
 requirements BOOLE, SUBSET;


begin

definition let r be number;
  attr r is real means
:: ARYTM:def 1
   r in REAL;
end;

definition
  cluster real number;
end;

definition let x,y be real number;
 func x + y means
:: ARYTM:def 2
  ex x',y' being Element of REAL+ st x = x' & y = y' & it = x' + y'
              if x in REAL+ & y in REAL+,
  ex x',y' being Element of REAL+ st x = x' & y = [{},y'] & it = x' - y'
              if x in REAL+ & y in [:{{}},REAL+:],
  ex x',y' being Element of REAL+ st x = [{},x'] & y = y' & it = y' - x'
              if y in REAL+ & x in [:{{}},REAL+:]
  otherwise
  ex x',y' being Element of REAL+ st x = [{},x'] & y = [{},y'] & it = [{}
,y'+x'];
  commutativity;

 func x * y means
:: ARYTM:def 3
  ex x',y' being Element of REAL+ st x = x' & y = y' & it = x' *' y'
              if x in REAL+ & y in REAL+,
  ex x',y' being Element of REAL+ st x = x' & y = [{},y'] & it = [{},x' *' y']
              if x in REAL+ & y in [:{{}},REAL+:] & x <> {},
  ex x',y' being Element of REAL+ st x = [{},x'] & y = y' & it = [{},y' *' x']
              if y in REAL+ & x in [:{{}},REAL+:] & y <> {},
  ex x',y' being Element of REAL+ st x = [{},x'] & y = [{},y'] & it = y' *' x'
              if x in [:{{}},REAL+:] & y in [:{{}},REAL+:]
   otherwise it = {};
  commutativity;
 pred x <= y means
:: ARYTM:def 4
  ex x',y' being Element of REAL+ st x = x' & y = y' & x' <=' y'
              if x in REAL+ & y in REAL+,
  ex x',y' being Element of REAL+ st x = [{},x'] & y = [{},y'] & y' <=' x'
              if x in [:{{}},REAL+:] & y in [:{{}},REAL+:]
  otherwise y in REAL+ & x in [:{{}},REAL+:];
  reflexivity;
  connectedness;
  synonym y >= x;
  antonym y < x;
  antonym x > y;
end;

definition let x,y be real number;
 cluster x + y -> real;
 cluster x * y -> real;
end;

definition
 cluster -> real Element of REAL;
end;

definition let x,y be Element of REAL;
  redefine func x + y -> Element of REAL;
  redefine func x * y -> Element of REAL;
end;

definition
 cluster natural -> real number;
end;