:: REAL_1 semantic presentation

registration
cluster -> real Element of REAL ;
coherence
for b1 being Element of REAL holds b1 is real
proof end;
end;

definition
mode Real is Element of REAL ;
end;

definition
let c1 be Real;
redefine func - as - c1 -> Real;
coherence
- c1 is Real by XREAL_0:def 1;
redefine func " as c1 " -> Real;
coherence
c1 " is Real by XREAL_0:def 1;
end;

definition
let c1, c2 be Real;
redefine func + as c1 + c2 -> Real;
coherence
c1 + c2 is Real by XREAL_0:def 1;
redefine func * as c1 * c2 -> Real;
coherence
c1 * c2 is Real by XREAL_0:def 1;
redefine func - as c1 - c2 -> Real;
coherence
c1 - c2 is Real by XREAL_0:def 1;
redefine func / as c1 / c2 -> Real;
coherence
c1 / c2 is Real by XREAL_0:def 1;
end;

theorem Th1: :: REAL_1:1
canceled;

theorem Th2: :: REAL_1:2
canceled;

theorem Th3: :: REAL_1:3
canceled;

theorem Th4: :: REAL_1:4
canceled;

theorem Th5: :: REAL_1:5
canceled;

theorem Th6: :: REAL_1:6
canceled;

theorem Th7: :: REAL_1:7
canceled;

theorem Th8: :: REAL_1:8
canceled;

theorem Th9: :: REAL_1:9
canceled;

theorem Th10: :: REAL_1:10
canceled;

theorem Th11: :: REAL_1:11
canceled;

theorem Th12: :: REAL_1:12
canceled;

theorem Th13: :: REAL_1:13
canceled;

theorem Th14: :: REAL_1:14
canceled;

theorem Th15: :: REAL_1:15
canceled;

theorem Th16: :: REAL_1:16
canceled;

theorem Th17: :: REAL_1:17
canceled;

theorem Th18: :: REAL_1:18
canceled;

theorem Th19: :: REAL_1:19
canceled;

theorem Th20: :: REAL_1:20
canceled;

theorem Th21: :: REAL_1:21
canceled;

theorem Th22: :: REAL_1:22
canceled;

theorem Th23: :: REAL_1:23
canceled;

theorem Th24: :: REAL_1:24
canceled;

theorem Th25: :: REAL_1:25
for b1 being real number holds b1 - 0 = b1 ;

theorem Th26: :: REAL_1:26
- 0 = 0 ;

definition
let c1, c2 be real number ;
canceled;
canceled;
canceled;
canceled;
redefine pred c1 <= c2 means :: REAL_1:def 5
( not a2 <= a1 or not a2 <> a1 );
compatibility
( not c2 < c1 iff ( not c2 <= c1 or not c2 <> c1 ) ) by XREAL_1:1;
end;

:: deftheorem Def1 REAL_1:def 1 :
canceled;

:: deftheorem Def2 REAL_1:def 2 :
canceled;

:: deftheorem Def3 REAL_1:def 3 :
canceled;

:: deftheorem Def4 REAL_1:def 4 :
canceled;

:: deftheorem Def5 defines < REAL_1:def 5 :
for b1, b2 being real number holds
( not b2 < b1 iff ( not b2 <= b1 or not b2 <> b1 ) );

theorem Th27: :: REAL_1:27
canceled;

theorem Th28: :: REAL_1:28
canceled;

theorem Th29: :: REAL_1:29
canceled;

theorem Th30: :: REAL_1:30
canceled;

theorem Th31: :: REAL_1:31
canceled;

theorem Th32: :: REAL_1:32
canceled;

theorem Th33: :: REAL_1:33
canceled;

theorem Th34: :: REAL_1:34
canceled;

theorem Th35: :: REAL_1:35
canceled;

theorem Th36: :: REAL_1:36
canceled;

theorem Th37: :: REAL_1:37
canceled;

theorem Th38: :: REAL_1:38
canceled;

theorem Th39: :: REAL_1:39
canceled;

theorem Th40: :: REAL_1:40
canceled;

theorem Th41: :: REAL_1:41
canceled;

theorem Th42: :: REAL_1:42
canceled;

theorem Th43: :: REAL_1:43
canceled;

theorem Th44: :: REAL_1:44
canceled;

theorem Th45: :: REAL_1:45
canceled;

theorem Th46: :: REAL_1:46
canceled;

theorem Th47: :: REAL_1:47
canceled;

theorem Th48: :: REAL_1:48
canceled;

theorem Th49: :: REAL_1:49
canceled;

theorem Th50: :: REAL_1:50
canceled;

theorem Th51: :: REAL_1:51
canceled;

theorem Th52: :: REAL_1:52
canceled;

theorem Th53: :: REAL_1:53
canceled;

theorem Th54: :: REAL_1:54
canceled;

theorem Th55: :: REAL_1:55
canceled;

theorem Th56: :: REAL_1:56
canceled;

theorem Th57: :: REAL_1:57
canceled;

theorem Th58: :: REAL_1:58
canceled;

theorem Th59: :: REAL_1:59
canceled;

theorem Th60: :: REAL_1:60
canceled;

theorem Th61: :: REAL_1:61
canceled;

theorem Th62: :: REAL_1:62
canceled;

theorem Th63: :: REAL_1:63
canceled;

theorem Th64: :: REAL_1:64
canceled;

theorem Th65: :: REAL_1:65
canceled;

theorem Th66: :: REAL_1:66
canceled;

theorem Th67: :: REAL_1:67
canceled;

theorem Th68: :: REAL_1:68
canceled;

theorem Th69: :: REAL_1:69
canceled;

theorem Th70: :: REAL_1:70
canceled;

theorem Th71: :: REAL_1:71
canceled;

theorem Th72: :: REAL_1:72
canceled;

theorem Th73: :: REAL_1:73
for b1, b2, b3 being real number st 0 < b1 holds
( b2 < b3 iff b2 / b1 < b3 / b1 ) by XREAL_1:74, XREAL_1:76;

theorem Th74: :: REAL_1:74
for b1, b2, b3 being real number st b1 < 0 holds
( b2 < b3 iff b3 / b1 < b2 / b1 ) by XREAL_1:75, XREAL_1:77;

scheme :: REAL_1:sch 1
s1{ P1[ Real] } :
ex b1 being Subset of REAL st
for b2 being Real holds
( b2 in b1 iff P1[b2] )
proof end;

theorem Th75: :: REAL_1:75
canceled;

theorem Th76: :: REAL_1:76
canceled;

theorem Th77: :: REAL_1:77
canceled;

theorem Th78: :: REAL_1:78
canceled;

theorem Th79: :: REAL_1:79
canceled;

theorem Th80: :: REAL_1:80
canceled;

theorem Th81: :: REAL_1:81
canceled;

theorem Th82: :: REAL_1:82
canceled;

theorem Th83: :: REAL_1:83
canceled;

theorem Th84: :: REAL_1:84
canceled;

theorem Th85: :: REAL_1:85
canceled;

theorem Th86: :: REAL_1:86
canceled;

theorem Th87: :: REAL_1:87
canceled;

theorem Th88: :: REAL_1:88
canceled;

theorem Th89: :: REAL_1:89
canceled;

theorem Th90: :: REAL_1:90
canceled;

theorem Th91: :: REAL_1:91
canceled;

theorem Th92: :: REAL_1:92
for b1, b2, b3, b4 being real number holds
( ( b1 <= b2 & b3 <= b4 implies b1 - b4 <= b2 - b3 ) & ( ( ( b1 < b2 & b3 <= b4 ) or ( b1 <= b2 & b3 < b4 ) ) implies b1 - b4 < b2 - b3 ) ) by XREAL_1:15, XREAL_1:16, XREAL_1:17;