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

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

proof end;

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

proof end;

Lm3: for x', y' being Element of REAL
for x, y being real number st x' = x & y' = y holds
+ x',y' = x + y

proof end;

Lm4: {} in {{} }
by TARSKI:def 1;

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

theorem :: AXIOMS:1

canceled;

theorem :: AXIOMS:2

canceled;

theorem :: AXIOMS:3

canceled;

theorem :: AXIOMS:4

canceled;

theorem :: AXIOMS:5

canceled;

theorem :: AXIOMS:6

canceled;

theorem :: AXIOMS:7

canceled;

theorem :: AXIOMS:8

canceled;

theorem :: AXIOMS:9

canceled;

theorem :: AXIOMS:10

canceled;

theorem :: AXIOMS:11

canceled;

theorem :: AXIOMS:12

canceled;

theorem :: AXIOMS:13

canceled;

theorem :: AXIOMS:14

canceled;

theorem :: AXIOMS:15

canceled;

theorem :: AXIOMS:16

canceled;

theorem :: AXIOMS:17

canceled;

theorem :: AXIOMS:18

canceled;

theorem :: AXIOMS:19

canceled;

theorem :: AXIOMS:20

canceled;

theorem :: AXIOMS:21

canceled;

theorem :: AXIOMS:22

canceled;

theorem :: AXIOMS:23

canceled;

theorem :: AXIOMS:24

canceled;

theorem :: AXIOMS:25

canceled;

theorem :: AXIOMS:26

for X, Y being Subset of REAL st ( for x, y being real number st x in X & y in Y holds
x <= y ) holds
ex z being real number st
for x, y being real number st x in X & y in Y holds
( x <= z & z <= y )

proof end;

theorem :: AXIOMS:27

canceled;

theorem :: AXIOMS:28

for x, y being real number st x in NAT & y in NAT holds
x + y in NAT

proof end;

theorem :: AXIOMS:29

for A being Subset of REAL st 0 in A & ( for x being real number st x in A holds
x + 1 in A ) holds
NAT c= A

proof end;

theorem :: AXIOMS:30

for k being natural number holds k = { i where i is Element of NAT : i < k }

proof end;