B.2 AXIOMS

AXIOMS. ABS (Digest)

reserve x, y, z for Any, X, X1, X2, X3, X4, Y for set;

3 z C [:X, Y:] iff ex x,y st x C X & y C Y & z = [x,y];
4 X is non empty implies ex x st x C X;
5 [: X1, X2, X3 :] = [:[:X1, X2:], X3:];
6 [: X1, X2, X3, X4 :] = [:[:X1, X2, X3:], X4:];

reserve x,y,z for Element of REAL;

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;
26 for X, Y being Subset of REAL st