B.2 AXIOMS

Strong Arithmetic of Real Numbers by Andrzej Trybulec

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

13 x + (y + z) = (x + y) + z;
16 x * (y * z) = (x * y) * z;
18 x * (y + z) = x * y + x * z;
19 ex y st x + y = 0;
20 x <> 0 implies ex y st x * y = 1;
21 x <= y & y <= x implies x = y;
22 x <= y & y <= z implies x <= z;
24 x <= y implies x + z <= y + z;
25 x <= y & 0 <= z implies x * z <= y * z;

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

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;
28 x in NAT & y in NAT implies x + y in NAT;
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;
30 k = { i: i < k };