:: AXIOMS semantic presentation

theorem Th1: :: AXIOMS:1
canceled;

theorem Th2: :: AXIOMS:2
canceled;

theorem Th3: :: AXIOMS:3
canceled;

theorem Th4: :: AXIOMS:4
canceled;

theorem Th5: :: AXIOMS:5
canceled;

theorem Th6: :: AXIOMS:6
canceled;

theorem Th7: :: AXIOMS:7
canceled;

theorem Th8: :: AXIOMS:8
canceled;

theorem Th9: :: AXIOMS:9
canceled;

theorem Th10: :: AXIOMS:10
canceled;

theorem Th11: :: AXIOMS:11
canceled;

theorem Th12: :: AXIOMS:12
canceled;

theorem Th13: :: AXIOMS:13
canceled;

theorem Th14: :: AXIOMS:14
canceled;

theorem Th15: :: AXIOMS:15
canceled;

theorem Th16: :: AXIOMS:16
canceled;

theorem Th17: :: AXIOMS:17
canceled;

theorem Th18: :: AXIOMS:18
canceled;

theorem Th19: :: AXIOMS:19
for b1 being real number ex b2 being real number st b1 + b2 = 0
proof end;

theorem Th20: :: AXIOMS:20
for b1 being real number st b1 <> 0 holds
ex b2 being real number st b1 * b2 = 1
proof end;

Lemma1: for b1, b2 being real number st b1 <= b2 & b2 <= b1 holds
b1 = b2
by XREAL_1:1;

Lemma2: for b1 being real number
for b2, b3 being Element of REAL st b1 = [*b2,b3*] holds
( b3 = 0 & b1 = b2 )
proof end;

Lemma3: for b1, b2 being Element of REAL
for b3, b4 being real number st b1 = b3 & b2 = b4 holds
+ b1,b2 = b3 + b4
proof end;

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

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

theorem Th21: :: AXIOMS:21
canceled;

theorem Th22: :: AXIOMS:22
canceled;

theorem Th23: :: AXIOMS:23
canceled;

theorem Th24: :: AXIOMS:24
canceled;

theorem Th25: :: AXIOMS:25
canceled;

theorem Th26: :: AXIOMS:26
for b1, b2 being Subset of REAL st ( for b3, b4 being real number st b3 in b1 & b4 in b2 holds
b3 <= b4 ) holds
ex b3 being real number st
for b4, b5 being real number st b4 in b1 & b5 in b2 holds
( b4 <= b3 & b3 <= b5 )
proof end;

theorem Th27: :: AXIOMS:27
canceled;

theorem Th28: :: AXIOMS:28
for b1, b2 being real number st b1 in NAT & b2 in NAT holds
b1 + b2 in NAT
proof end;

E5: one = succ 0 by ORDINAL2:def 4
.= 1 ;

theorem Th29: :: AXIOMS:29
for b1 being Subset of REAL st 0 in b1 & ( for b2 being real number st b2 in b1 holds
b2 + 1 in b1 ) holds
NAT c= b1
proof end;

theorem Th30: :: AXIOMS:30
for b1 being natural number holds b1 = { b2 where B is Element of NAT : b2 < b1 }
proof end;