Lm1:
omega c= ( { [c,d] where c, d is Element of omega : ( c,d are_coprime & d <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega
by XBOOLE_1:7;
Lm2:
1 = succ 0
;
Lm3:
REAL+ c= REAL
Lm4:
RAT+ c= RAT
Lm5:
NAT c= INT
Lm6:
for x, y, z being set st [x,y] = {z} holds
( z = {x} & x = y )
Lm7:
for a, b being Element of REAL holds not (0,one) --> (a,b) in REAL
Lm8:
RAT c= REAL
Lm9:
for i, j being ordinal Element of RAT+ st i in j holds
i < j
Lm10:
for i, j being ordinal Element of RAT+ st i c= j holds
i <=' j
Lm11: 2 =
succ 1
.=
(succ 0) \/ {1}
.=
(0 \/ {0}) \/ {1}
.=
{0,1}
by ENUMSET1:1
;
Lm12:
for i, k being natural Ordinal st i *^ i = 2 *^ k holds
ex k being natural Ordinal st i = 2 *^ k
reconsider a9 = 1 as Element of RAT+ by Lm1;
reconsider two = 2 as ordinal Element of RAT+ by Lm1;
Lm13:
one + one = two
Lm14:
for i being Element of RAT+ holds i + i = two *' i
Lm15:
INT c= RAT