:: XREAL_1 semantic presentation

theorem Th1: :: XREAL_1:1

for b₁, b₂ being real number st b₁ <= b₂ & b₂ <= b₁ holds
b₁ = b₂

proof end;

theorem Th2: :: XREAL_1:2

for b₁, b₂, b₃ being real number st b₁ <= b₂ & b₂ <= b₃ holds
b₁ <= b₃

proof end;

Lemma3: for b₁ being real number
for b₂, b₃ being Element of REAL st b₁ = [*b₂,b₃*] holds
( b₃ = 0 & b₁ = b₂ )

proof end;

Lemma4: for b₁, b₂ being Element of REAL
for b₃, b₄ being real number st b₁ = b₃ & b₂ = b₄ holds
+ b₁,b₂ = b₃ + b₄

proof end;

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

Lemma6: for b₁, b₂, b₃ being real number st b₁ <= b₂ holds
b₁ + b₃ <= b₂ + b₃

proof end;

Lemma7: for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
b₁ + b₃ <= b₂ + b₄

proof end;

Lemma8: for b₁, b₂, b₃ being real number st b₁ <= b₂ holds
b₁ - b₃ <= b₂ - b₃

proof end;

Lemma9: for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ & b₃ <= b₄ holds
b₁ + b₃ < b₂ + b₄

proof end;

Lemma10: for b₁, b₂ being real number st 0 < b₁ holds
b₂ < b₂ + b₁

proof end;

theorem Th3: :: XREAL_1:3

for b₁ being real number ex b₂ being real number st b₁ < b₂

proof end;

theorem Th4: :: XREAL_1:4

for b₁ being real number ex b₂ being real number st b₂ < b₁

proof end;

theorem Th5: :: XREAL_1:5

for b₁, b₂ being real number ex b₃ being real number st
( b₁ < b₃ & b₂ < b₃ )

proof end;

Lemma11: for b₁, b₂, b₃ being real number st b₁ + b₂ <= b₃ + b₂ holds
b₁ <= b₃

proof end;

theorem Th6: :: XREAL_1:6

for b₁, b₂ being real number ex b₃ being real number st
( b₃ < b₁ & b₃ < b₂ )

proof end;

Lemma12: for b₁, b₂ being Element of REAL
for b₃, b₄ being real number st b₁ = b₃ & b₂ = b₄ holds
* b₁,b₂ = b₃ * b₄

proof end;

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

Lemma13: for b₁, b₂, b₃ being real number st b₁ <= b₂ & 0 <= b₃ holds
b₁ * b₃ <= b₂ * b₃

proof end;

Lemma14: for b₁, b₂, b₃ being real number st 0 < b₁ & b₂ < b₃ holds
b₂ * b₁ < b₃ * b₁

proof end;

theorem Th7: :: XREAL_1:7

for b₁, b₂ being real number st b₁ < b₂ holds
ex b₃ being real number st
( b₁ < b₃ & b₃ < b₂ )

proof end;

theorem Th8: :: XREAL_1:8

for b₁, b₂, b₃ being real number holds
( b₁ <= b₂ iff b₁ + b₃ <= b₂ + b₃ ) by Lemma6, Lemma11;

theorem Th9: :: XREAL_1:9

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
b₁ + b₃ <= b₂ + b₄ by Lemma7;

theorem Th10: :: XREAL_1:10

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ & b₃ <= b₄ holds
b₁ + b₃ < b₂ + b₄ by Lemma9;

Lemma16: for b₁, b₂ being real number st b₁ <= b₂ holds
- b₂ <= - b₁

proof end;

Lemma17: for b₁, b₂ being real number st - b₁ <= - b₂ holds
b₂ <= b₁

proof end;

theorem Th11: :: XREAL_1:11

for b₁, b₂, b₃ being real number holds
( b₁ <= b₂ iff b₁ - b₃ <= b₂ - b₃ )

proof end;

theorem Th12: :: XREAL_1:12

for b₁, b₂, b₃ being real number holds
( b₁ <= b₂ iff b₃ - b₂ <= b₃ - b₁ )

proof end;

Lemma19: for b₁, b₂, b₃ being real number st b₁ + b₂ <= b₃ holds
b₁ <= b₃ - b₂

proof end;

Lemma20: for b₁, b₂, b₃ being real number st b₁ <= b₂ - b₃ holds
b₁ + b₃ <= b₂

proof end;

Lemma21: for b₁, b₂, b₃ being real number st b₁ <= b₂ + b₃ holds
b₁ - b₂ <= b₃

proof end;

Lemma22: for b₁, b₂, b₃ being real number st b₁ - b₂ <= b₃ holds
b₁ <= b₂ + b₃

proof end;

theorem Th13: :: XREAL_1:13

for b₁, b₂, b₃ being real number st b₁ <= b₂ - b₃ holds
b₃ <= b₂ - b₁

proof end;

theorem Th14: :: XREAL_1:14

for b₁, b₂, b₃ being real number st b₁ - b₂ <= b₃ holds
b₁ - b₃ <= b₂

proof end;

theorem Th15: :: XREAL_1:15

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
b₁ - b₄ <= b₂ - b₃

proof end;

theorem Th16: :: XREAL_1:16

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ & b₃ <= b₄ holds
b₁ - b₄ < b₂ - b₃

proof end;

theorem Th17: :: XREAL_1:17

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ < b₄ holds
b₁ - b₄ < b₂ - b₃

proof end;

Lemma25: for b₁, b₂, b₃, b₄ being real number st b₁ + b₂ <= b₃ + b₄ holds
b₁ - b₃ <= b₄ - b₂

proof end;

theorem Th18: :: XREAL_1:18

for b₁, b₂, b₃, b₄ being real number st b₁ - b₂ <= b₃ - b₄ holds
b₁ - b₃ <= b₂ - b₄

proof end;

theorem Th19: :: XREAL_1:19

for b₁, b₂, b₃, b₄ being real number st b₁ - b₂ <= b₃ - b₄ holds
b₄ - b₂ <= b₃ - b₁

proof end;

theorem Th20: :: XREAL_1:20

for b₁, b₂, b₃, b₄ being real number st b₁ - b₂ <= b₃ - b₄ holds
b₄ - b₃ <= b₂ - b₁

proof end;

theorem Th21: :: XREAL_1:21

for b₁, b₂, b₃ being real number holds
( b₁ + b₂ <= b₃ iff b₁ <= b₃ - b₂ ) by Lemma19, Lemma20;

theorem Th22: :: XREAL_1:22

for b₁, b₂, b₃ being real number holds
( b₁ <= b₂ + b₃ iff b₁ - b₂ <= b₃ ) by Lemma21, Lemma22;

theorem Th23: :: XREAL_1:23

for b₁, b₂, b₃, b₄ being real number holds
( b₁ + b₂ <= b₃ + b₄ iff b₁ - b₃ <= b₄ - b₂ )

proof end;

theorem Th24: :: XREAL_1:24

for b₁, b₂, b₃, b₄ being real number st b₁ + b₂ <= b₃ - b₄ holds
b₁ + b₄ <= b₃ - b₂

proof end;

theorem Th25: :: XREAL_1:25

for b₁, b₂, b₃, b₄ being real number st b₁ - b₂ <= b₃ + b₄ holds
b₁ - b₄ <= b₃ + b₂

proof end;

theorem Th26: :: XREAL_1:26

for b₁, b₂ being real number holds
( b₁ <= b₂ iff - b₂ <= - b₁ ) by Lemma16, Lemma17;

Lemma26: for b₁, b₂ being real number st b₁ < b₂ holds
0 < b₂ - b₁

proof end;

theorem Th27: :: XREAL_1:27

for b₁, b₂ being real number st b₁ <= - b₂ holds
b₂ <= - b₁

proof end;

Lemma28: for b₁, b₂ being real number st b₁ <= b₂ holds
0 <= b₂ - b₁

proof end;

theorem Th28: :: XREAL_1:28

for b₁, b₂ being real number st - b₁ <= b₂ holds
- b₂ <= b₁

proof end;

theorem Th29: :: XREAL_1:29

for b₁, b₂ being real number st 0 <= b₁ & 0 <= b₂ & b₁ + b₂ = 0 holds
b₁ = 0

proof end;

theorem Th30: :: XREAL_1:30

for b₁, b₂ being real number st b₁ <= 0 & b₂ <= 0 & b₁ + b₂ = 0 holds
b₁ = 0

proof end;

theorem Th31: :: XREAL_1:31

for b₁, b₂ being real number st 0 < b₁ holds
b₂ < b₂ + b₁ by Lemma10;

theorem Th32: :: XREAL_1:32

for b₁, b₂ being real number st b₁ < 0 holds
b₁ + b₂ < b₂

proof end;

Lemma31: for b₁, b₂ being real number st b₁ < b₂ holds
b₁ - b₂ < 0

proof end;

Lemma32: for b₁ being real number holds
( b₁ < 0 iff 0 < - b₁ )

proof end;

theorem Th33: :: XREAL_1:33

for b₁, b₂ being real number st 0 <= b₁ holds
b₂ <= b₁ + b₂

proof end;

theorem Th34: :: XREAL_1:34

for b₁, b₂ being real number st b₁ <= 0 holds
b₁ + b₂ <= b₂

proof end;

theorem Th35: :: XREAL_1:35

for b₁, b₂ being real number st 0 <= b₁ & 0 <= b₂ holds
0 <= b₁ + b₂

proof end;

theorem Th36: :: XREAL_1:36

for b₁, b₂ being real number st 0 <= b₁ & 0 < b₂ holds
0 < b₁ + b₂

proof end;

theorem Th37: :: XREAL_1:37

for b₁, b₂, b₃ being real number st b₁ <= 0 & b₂ <= b₃ holds
b₂ + b₁ <= b₃

proof end;

theorem Th38: :: XREAL_1:38

for b₁, b₂, b₃ being real number st b₁ <= 0 & b₂ < b₃ holds
b₂ + b₁ < b₃

proof end;

theorem Th39: :: XREAL_1:39

for b₁, b₂, b₃ being real number st b₁ < 0 & b₂ <= b₃ holds
b₂ + b₁ < b₃

proof end;

theorem Th40: :: XREAL_1:40

for b₁, b₂, b₃ being real number st 0 <= b₁ & b₂ <= b₃ holds
b₂ <= b₁ + b₃

proof end;

theorem Th41: :: XREAL_1:41

for b₁, b₂, b₃ being real number st 0 < b₁ & b₂ <= b₃ holds
b₂ < b₁ + b₃

proof end;

theorem Th42: :: XREAL_1:42

for b₁, b₂, b₃ being real number st 0 <= b₁ & b₂ < b₃ holds
b₂ < b₁ + b₃

proof end;

Lemma37: for b₁, b₂, b₃ being real number st b₁ < 0 & b₂ < b₃ holds
b₃ * b₁ < b₂ * b₁

proof end;

Lemma38: for b₁ being real number st 0 < b₁ holds
0 < b₁ "

proof end;

Lemma39: for b₁, b₂, b₃ being real number st 0 <= b₁ & b₂ <= b₃ holds
b₂ / b₁ <= b₃ / b₁

proof end;

Lemma40: for b₁, b₂, b₃ being real number st 0 < b₁ & b₂ < b₃ holds
b₂ / b₁ < b₃ / b₁

proof end;

Lemma41: for b₁ being real number st 0 < b₁ holds
0 < b₁ / 2

proof end;

Lemma42: for b₁ being real number st 0 < b₁ holds
b₁ / 2 < b₁

proof end;

theorem Th43: :: XREAL_1:43

for b₁, b₂ being real number st ( for b₃ being real number st b₃ > 0 holds
b₁ <= b₂ + b₃ ) holds
b₁ <= b₂

proof end;

theorem Th44: :: XREAL_1:44

for b₁, b₂ being real number st ( for b₃ being real number st b₃ < 0 holds
b₁ + b₃ <= b₂ ) holds
b₁ <= b₂

proof end;

theorem Th45: :: XREAL_1:45

for b₁, b₂ being real number st 0 <= b₁ holds
b₂ - b₁ <= b₂

proof end;

theorem Th46: :: XREAL_1:46

for b₁, b₂ being real number st 0 < b₁ holds
b₂ - b₁ < b₂

proof end;

theorem Th47: :: XREAL_1:47

for b₁, b₂ being real number st b₁ <= 0 holds
b₂ <= b₂ - b₁

proof end;

theorem Th48: :: XREAL_1:48

for b₁, b₂ being real number st b₁ < 0 holds
b₂ < b₂ - b₁

proof end;

theorem Th49: :: XREAL_1:49

for b₁, b₂ being real number st b₁ <= b₂ holds
b₁ - b₂ <= 0

proof end;

theorem Th50: :: XREAL_1:50

for b₁, b₂ being real number st b₁ <= b₂ holds
0 <= b₂ - b₁

proof end;

theorem Th51: :: XREAL_1:51

for b₁, b₂ being real number st b₁ < b₂ holds
b₁ - b₂ < 0 by Lemma31;

theorem Th52: :: XREAL_1:52

for b₁, b₂ being real number st b₁ < b₂ holds
0 < b₂ - b₁ by Lemma26;

theorem Th53: :: XREAL_1:53

for b₁, b₂, b₃ being real number st 0 <= b₁ & b₂ < b₃ holds
b₂ - b₁ < b₃

proof end;

theorem Th54: :: XREAL_1:54

for b₁, b₂, b₃ being real number st b₁ <= 0 & b₂ <= b₃ holds
b₂ <= b₃ - b₁

proof end;

theorem Th55: :: XREAL_1:55

for b₁, b₂, b₃ being real number st b₁ <= 0 & b₂ < b₃ holds
b₂ < b₃ - b₁

proof end;

theorem Th56: :: XREAL_1:56

for b₁, b₂, b₃ being real number st b₁ < 0 & b₂ <= b₃ holds
b₂ < b₃ - b₁

proof end;

theorem Th57: :: XREAL_1:57

for b₁, b₂ being real number holds
( not b₁ <> b₂ or 0 < b₁ - b₂ or 0 < b₂ - b₁ )

proof end;

theorem Th58: :: XREAL_1:58

for b₁, b₂ being real number st ( for b₃ being real number st b₃ < 0 holds
b₁ <= b₂ - b₃ ) holds
b₂ >= b₁

proof end;

theorem Th59: :: XREAL_1:59

for b₁, b₂ being real number st ( for b₃ being real number st b₃ > 0 holds
b₁ - b₃ <= b₂ ) holds
b₁ <= b₂

proof end;

theorem Th60: :: XREAL_1:60

for b₁ being real number holds
( b₁ < 0 iff 0 < - b₁ ) by Lemma32;

theorem Th61: :: XREAL_1:61

for b₁, b₂ being real number st b₁ <= - b₂ holds
b₁ + b₂ <= 0

proof end;

theorem Th62: :: XREAL_1:62

for b₁, b₂ being real number st - b₁ <= b₂ holds
0 <= b₁ + b₂

proof end;

theorem Th63: :: XREAL_1:63

for b₁, b₂ being real number st b₁ < - b₂ holds
b₁ + b₂ < 0

proof end;

theorem Th64: :: XREAL_1:64

for b₁, b₂ being real number st - b₁ < b₂ holds
0 < b₂ + b₁

proof end;

Lemma44: for b₁, b₂, b₃ being real number st b₁ <= b₂ & b₃ <= 0 holds
b₂ * b₃ <= b₁ * b₃

proof end;

theorem Th65: :: XREAL_1:65

for b₁ being real number holds 0 <= b₁ * b₁

proof end;

theorem Th66: :: XREAL_1:66

for b₁, b₂, b₃ being real number st b₁ <= b₂ & 0 <= b₃ holds
b₁ * b₃ <= b₂ * b₃ by Lemma13;

theorem Th67: :: XREAL_1:67

for b₁, b₂, b₃ being real number st b₁ <= b₂ & b₃ <= 0 holds
b₂ * b₃ <= b₁ * b₃ by Lemma44;

theorem Th68: :: XREAL_1:68

for b₁, b₂, b₃, b₄ being real number st 0 <= b₁ & b₁ <= b₂ & 0 <= b₃ & b₃ <= b₄ holds
b₁ * b₃ <= b₂ * b₄

proof end;

theorem Th69: :: XREAL_1:69

for b₁, b₂, b₃, b₄ being real number st b₁ <= 0 & b₂ <= b₁ & b₃ <= 0 & b₄ <= b₃ holds
b₁ * b₃ <= b₂ * b₄

proof end;

theorem Th70: :: XREAL_1:70

for b₁, b₂, b₃ being real number st 0 < b₁ & b₂ < b₃ holds
b₂ * b₁ < b₃ * b₁ by Lemma14;

theorem Th71: :: XREAL_1:71

for b₁, b₂, b₃ being real number st b₁ < 0 & b₂ < b₃ holds
b₃ * b₁ < b₂ * b₁ by Lemma37;

theorem Th72: :: XREAL_1:72

for b₁, b₂, b₃, b₄ being real number st b₁ < 0 & b₂ <= b₁ & b₃ < 0 & b₄ < b₃ holds
b₁ * b₃ < b₂ * b₄

proof end;

theorem Th73: :: XREAL_1:73

for b₁, b₂, b₃, b₄ being real number st 0 <= b₁ & 0 <= b₂ & 0 <= b₃ & 0 <= b₄ & (b₁ * b₃) + (b₂ * b₄) = 0 & not b₁ = 0 holds
b₃ = 0

proof end;

Lemma47: for b₁, b₂, b₃ being real number st b₁ < 0 & b₂ < b₃ holds
b₃ / b₁ < b₂ / b₁

proof end;

Lemma48: for b₁, b₂, b₃ being real number st b₁ <= 0 & b₂ / b₁ < b₃ / b₁ holds
b₃ < b₂

proof end;

theorem Th74: :: XREAL_1:74

for b₁, b₂, b₃ being real number st 0 <= b₁ & b₂ <= b₃ holds
b₂ / b₁ <= b₃ / b₁ by Lemma39;

theorem Th75: :: XREAL_1:75

for b₁, b₂, b₃ being real number st b₁ <= 0 & b₂ <= b₃ holds
b₃ / b₁ <= b₂ / b₁ by Lemma48;

theorem Th76: :: XREAL_1:76

for b₁, b₂, b₃ being real number st 0 < b₁ & b₂ < b₃ holds
b₂ / b₁ < b₃ / b₁ by Lemma40;

theorem Th77: :: XREAL_1:77

for b₁, b₂, b₃ being real number st b₁ < 0 & b₂ < b₃ holds
b₃ / b₁ < b₂ / b₁ by Lemma47;

theorem Th78: :: XREAL_1:78

for b₁, b₂, b₃ being real number st 0 < b₁ & 0 < b₂ & b₂ < b₃ holds
b₁ / b₃ < b₁ / b₂

proof end;

Lemma49: for b₁, b₂ being real number st b₁ < 0 & 0 < b₂ holds
b₂ / b₁ < 0

proof end;

Lemma50: for b₁, b₂ being real number st b₁ < 0 & b₂ < b₁ holds
b₁ " < b₂ "

proof end;

theorem Th79: :: XREAL_1:79

for b₁, b₂, b₃ being real number st 0 < b₁ & b₂ * b₁ <= b₃ holds
b₂ <= b₃ / b₁

proof end;

theorem Th80: :: XREAL_1:80

for b₁, b₂, b₃ being real number st b₁ < 0 & b₂ * b₁ <= b₃ holds
b₃ / b₁ <= b₂

proof end;

theorem Th81: :: XREAL_1:81

for b₁, b₂, b₃ being real number st 0 < b₁ & b₂ <= b₃ * b₁ holds
b₂ / b₁ <= b₃

proof end;

theorem Th82: :: XREAL_1:82

for b₁, b₂, b₃ being real number st b₁ < 0 & b₂ <= b₃ * b₁ holds
b₃ <= b₂ / b₁

proof end;

theorem Th83: :: XREAL_1:83

for b₁, b₂, b₃ being real number st 0 < b₁ & b₂ * b₁ < b₃ holds
b₂ < b₃ / b₁

proof end;

theorem Th84: :: XREAL_1:84

for b₁, b₂, b₃ being real number st b₁ < 0 & b₂ * b₁ < b₃ holds
b₃ / b₁ < b₂

proof end;

theorem Th85: :: XREAL_1:85

for b₁, b₂, b₃ being real number st 0 < b₁ & b₂ < b₃ * b₁ holds
b₂ / b₁ < b₃

proof end;

theorem Th86: :: XREAL_1:86

for b₁, b₂, b₃ being real number st b₁ < 0 & b₂ < b₃ * b₁ holds
b₃ < b₂ / b₁

proof end;

Lemma59: for b₁, b₂ being real number st 0 < b₁ & b₁ <= b₂ holds
b₂ " <= b₁ "

proof end;

Lemma60: for b₁, b₂ being real number st b₁ < 0 & b₂ <= b₁ holds
b₁ " <= b₂ "

proof end;

theorem Th87: :: XREAL_1:87

for b₁, b₂ being real number st 0 < b₁ & b₁ <= b₂ holds
b₂ " <= b₁ " by Lemma59;

theorem Th88: :: XREAL_1:88

for b₁, b₂ being real number st b₁ < 0 & b₂ <= b₁ holds
b₁ " <= b₂ " by Lemma60;

theorem Th89: :: XREAL_1:89

for b₁, b₂ being real number st b₁ < 0 & b₂ < b₁ holds
b₁ " < b₂ " by Lemma50;

Lemma61: for b₁, b₂ being real number st 0 < b₁ & 0 < b₂ holds
0 < b₁ / b₂

proof end;

Lemma62: for b₁, b₂ being real number st 0 < b₁ & b₁ < b₂ holds
b₂ " < b₁ "

proof end;

theorem Th90: :: XREAL_1:90

for b₁, b₂ being real number st 0 < b₁ & b₁ < b₂ holds
b₂ " < b₁ " by Lemma62;

theorem Th91: :: XREAL_1:91

for b₁, b₂ being real number st 0 < b₁ " & b₁ " <= b₂ " holds
b₂ <= b₁

proof end;

theorem Th92: :: XREAL_1:92

for b₁, b₂ being real number st b₁ " < 0 & b₂ " <= b₁ " holds
b₁ <= b₂

proof end;

theorem Th93: :: XREAL_1:93

for b₁, b₂ being real number st 0 < b₁ " & b₁ " < b₂ " holds
b₂ < b₁

proof end;

theorem Th94: :: XREAL_1:94

for b₁, b₂ being real number st b₁ " < 0 & b₂ " < b₁ " holds
b₁ < b₂

proof end;

Lemma63: for b₁, b₂ being real positive number holds 0 < b₁ * b₂
;

Lemma64: for b₁, b₂ being real negative number holds 0 < b₁ * b₂
;

Lemma65: for b₁, b₂ being real non negative number holds 0 <= b₁ * b₂
;

Lemma66: for b₁, b₂ being real non positive number holds 0 <= b₁ * b₂
;

Lemma67: for b₁ being real number
for b₂ being real non positive non negative number holds 0 = b₂ * b₁
;

Lemma68: for b₁ being real positive number
for b₂ being real negative number holds b₁ * b₂ < 0
;

theorem Th95: :: XREAL_1:95

for b₁, b₂ being real number st 0 <= b₁ & (b₂ - b₁) * (b₂ + b₁) <= 0 holds
( - b₁ <= b₂ & b₂ <= b₁ )

proof end;

theorem Th96: :: XREAL_1:96

for b₁, b₂ being real number st 0 <= b₁ & (b₂ - b₁) * (b₂ + b₁) < 0 holds
( - b₁ < b₂ & b₂ < b₁ )

proof end;

theorem Th97: :: XREAL_1:97

for b₁, b₂ being real number st 0 <= b₁ & 0 <= (b₂ - b₁) * (b₂ + b₁) & not b₂ <= - b₁ holds
b₁ <= b₂

proof end;

theorem Th98: :: XREAL_1:98

for b₁, b₂, b₃, b₄ being real number st 0 <= b₁ & 0 <= b₂ & b₁ < b₃ & b₂ < b₄ holds
b₁ * b₂ < b₃ * b₄

proof end;

theorem Th99: :: XREAL_1:99

for b₁, b₂, b₃, b₄ being real number st 0 <= b₁ & 0 < b₂ & b₁ < b₃ & b₂ <= b₄ holds
b₁ * b₂ < b₃ * b₄

proof end;

theorem Th100: :: XREAL_1:100

for b₁, b₂, b₃, b₄ being real number st 0 < b₁ & 0 < b₂ & b₁ <= b₃ & b₂ < b₄ holds
b₁ * b₂ < b₃ * b₄

proof end;

theorem Th101: :: XREAL_1:101

for b₁, b₂, b₃ being real number st 0 < b₁ & b₂ < 0 & b₃ < b₂ holds
b₁ / b₂ < b₁ / b₃

proof end;

theorem Th102: :: XREAL_1:102

for b₁, b₂, b₃ being real number st b₁ < 0 & 0 < b₂ & b₂ < b₃ holds
b₁ / b₂ < b₁ / b₃

proof end;

theorem Th103: :: XREAL_1:103

for b₁, b₂, b₃ being real number st b₁ < 0 & b₂ < 0 & b₃ < b₂ holds
b₁ / b₃ < b₁ / b₂

proof end;

theorem Th104: :: XREAL_1:104

for b₁, b₂, b₃, b₄ being real number st 0 < b₁ & 0 < b₂ & b₃ * b₂ <= b₄ * b₁ holds
b₃ / b₁ <= b₄ / b₂

proof end;

theorem Th105: :: XREAL_1:105

for b₁, b₂, b₃, b₄ being real number st b₁ < 0 & b₂ < 0 & b₃ * b₂ <= b₄ * b₁ holds
b₃ / b₁ <= b₄ / b₂

proof end;

theorem Th106: :: XREAL_1:106

for b₁, b₂, b₃, b₄ being real number st 0 < b₁ & b₂ < 0 & b₃ * b₂ <= b₄ * b₁ holds
b₄ / b₂ <= b₃ / b₁

proof end;

theorem Th107: :: XREAL_1:107

for b₁, b₂, b₃, b₄ being real number st b₁ < 0 & 0 < b₂ & b₃ * b₂ <= b₄ * b₁ holds
b₄ / b₂ <= b₃ / b₁

proof end;

theorem Th108: :: XREAL_1:108

for b₁, b₂, b₃, b₄ being real number st 0 < b₁ & 0 < b₂ & b₃ * b₂ < b₄ * b₁ holds
b₃ / b₁ < b₄ / b₂

proof end;

theorem Th109: :: XREAL_1:109

for b₁, b₂, b₃, b₄ being real number st b₁ < 0 & b₂ < 0 & b₃ * b₂ < b₄ * b₁ holds
b₃ / b₁ < b₄ / b₂

proof end;

theorem Th110: :: XREAL_1:110

for b₁, b₂, b₃, b₄ being real number st 0 < b₁ & b₂ < 0 & b₃ * b₂ < b₄ * b₁ holds
b₄ / b₂ < b₃ / b₁

proof end;

theorem Th111: :: XREAL_1:111

for b₁, b₂, b₃, b₄ being real number st b₁ < 0 & 0 < b₂ & b₃ * b₂ < b₄ * b₁ holds
b₄ / b₂ < b₃ / b₁

proof end;

theorem Th112: :: XREAL_1:112

for b₁, b₂, b₃, b₄ being real number st b₁ < 0 & b₂ < 0 & b₃ * b₁ < b₄ / b₂ holds
b₃ * b₂ < b₄ / b₁

proof end;

theorem Th113: :: XREAL_1:113

for b₁, b₂, b₃, b₄ being real number st 0 < b₁ & 0 < b₂ & b₃ * b₁ < b₄ / b₂ holds
b₃ * b₂ < b₄ / b₁

proof end;

theorem Th114: :: XREAL_1:114

for b₁, b₂, b₃, b₄ being real number st b₁ < 0 & b₂ < 0 & b₃ / b₂ < b₄ * b₁ holds
b₃ / b₁ < b₄ * b₂

proof end;

theorem Th115: :: XREAL_1:115

for b₁, b₂, b₃, b₄ being real number st 0 < b₁ & 0 < b₂ & b₃ / b₂ < b₄ * b₁ holds
b₃ / b₁ < b₄ * b₂

proof end;

theorem Th116: :: XREAL_1:116

for b₁, b₂, b₃, b₄ being real number st b₁ < 0 & 0 < b₂ & b₃ * b₁ < b₄ / b₂ holds
b₄ / b₁ < b₃ * b₂

proof end;

theorem Th117: :: XREAL_1:117

for b₁, b₂, b₃, b₄ being real number st 0 < b₁ & b₂ < 0 & b₃ * b₁ < b₄ / b₂ holds
b₄ / b₁ < b₃ * b₂

proof end;

theorem Th118: :: XREAL_1:118

for b₁, b₂, b₃, b₄ being real number st b₁ < 0 & 0 < b₂ & b₃ / b₂ < b₄ * b₁ holds
b₄ * b₂ < b₃ / b₁

proof end;

theorem Th119: :: XREAL_1:119

for b₁, b₂, b₃, b₄ being real number st 0 < b₁ & b₂ < 0 & b₃ / b₂ < b₄ * b₁ holds
b₄ * b₂ < b₃ / b₁

proof end;

theorem Th120: :: XREAL_1:120

for b₁, b₂, b₃ being real number st 0 < b₁ & 0 <= b₂ & b₁ <= b₃ holds
b₂ / b₃ <= b₂ / b₁

proof end;

theorem Th121: :: XREAL_1:121

for b₁, b₂, b₃ being real number st 0 <= b₁ & b₂ < 0 & b₃ <= b₂ holds
b₁ / b₂ <= b₁ / b₃

proof end;

theorem Th122: :: XREAL_1:122

for b₁, b₂, b₃ being real number st b₁ <= 0 & 0 < b₂ & b₂ <= b₃ holds
b₁ / b₂ <= b₁ / b₃

proof end;

theorem Th123: :: XREAL_1:123

for b₁, b₂, b₃ being real number st b₁ <= 0 & b₂ < 0 & b₃ <= b₂ holds
b₁ / b₃ <= b₁ / b₂

proof end;

theorem Th124: :: XREAL_1:124

for b₁ being real number holds
( 0 < b₁ iff 0 < b₁ " )

proof end;

theorem Th125: :: XREAL_1:125

for b₁ being real number holds
( b₁ < 0 iff b₁ " < 0 )

proof end;

theorem Th126: :: XREAL_1:126

for b₁, b₂ being real number st b₁ < 0 & 0 < b₂ holds
b₁ " < b₂ "

proof end;

theorem Th127: :: XREAL_1:127

for b₁, b₂ being real number st b₁ " < 0 & 0 < b₂ " holds
b₁ < b₂

proof end;

theorem Th128: :: XREAL_1:128

for b₁, b₂ being real number st b₁ <= 0 & 0 <= b₁ holds
0 = b₁ * b₂ by Lemma67;

theorem Th129: :: XREAL_1:129

for b₁, b₂ being real number st 0 <= b₁ & 0 <= b₂ holds
0 <= b₁ * b₂ by Lemma65;

theorem Th130: :: XREAL_1:130

for b₁, b₂ being real number st b₁ <= 0 & b₂ <= 0 holds
0 <= b₁ * b₂ by Lemma66;

theorem Th131: :: XREAL_1:131

for b₁, b₂ being real number st 0 < b₁ & 0 < b₂ holds
0 < b₁ * b₂ by Lemma63;

theorem Th132: :: XREAL_1:132

for b₁, b₂ being real number st b₁ < 0 & b₂ < 0 holds
0 < b₁ * b₂ by Lemma64;

theorem Th133: :: XREAL_1:133

for b₁, b₂ being real number st 0 <= b₁ & b₂ <= 0 holds
b₁ * b₂ <= 0

proof end;

theorem Th134: :: XREAL_1:134

for b₁, b₂ being real number st 0 < b₁ & b₂ < 0 holds
b₁ * b₂ < 0 by Lemma68;

theorem Th135: :: XREAL_1:135

for b₁, b₂ being real number holds
( not b₁ * b₂ < 0 or ( b₁ > 0 & b₂ < 0 ) or ( b₁ < 0 & b₂ > 0 ) )

proof end;

theorem Th136: :: XREAL_1:136

for b₁, b₂ being real number holds
( not b₁ * b₂ > 0 or ( b₁ > 0 & b₂ > 0 ) or ( b₁ < 0 & b₂ < 0 ) )

proof end;

theorem Th137: :: XREAL_1:137

for b₁, b₂ being real number st b₁ <= 0 & b₂ <= 0 holds
0 <= b₁ / b₂

proof end;

theorem Th138: :: XREAL_1:138

for b₁, b₂ being real number st 0 <= b₁ & 0 <= b₂ holds
0 <= b₁ / b₂

proof end;

theorem Th139: :: XREAL_1:139

for b₁, b₂ being real number st 0 <= b₁ & b₂ <= 0 holds
b₁ / b₂ <= 0

proof end;

theorem Th140: :: XREAL_1:140

for b₁, b₂ being real number st b₁ <= 0 & 0 <= b₂ holds
b₁ / b₂ <= 0

proof end;

theorem Th141: :: XREAL_1:141

for b₁, b₂ being real number st 0 < b₁ & 0 < b₂ holds
0 < b₁ / b₂ by Lemma61;

theorem Th142: :: XREAL_1:142

for b₁, b₂ being real number st b₁ < 0 & b₂ < 0 holds
0 < b₁ / b₂

proof end;

theorem Th143: :: XREAL_1:143

for b₁, b₂ being real number st b₁ < 0 & 0 < b₂ holds
b₁ / b₂ < 0

proof end;

theorem Th144: :: XREAL_1:144

for b₁, b₂ being real number st b₁ < 0 & 0 < b₂ holds
b₂ / b₁ < 0 by Lemma49;

theorem Th145: :: XREAL_1:145

for b₁, b₂ being real number holds
( not b₁ / b₂ < 0 or ( b₂ < 0 & b₁ > 0 ) or ( b₂ > 0 & b₁ < 0 ) )

proof end;

theorem Th146: :: XREAL_1:146

for b₁, b₂ being real number holds
( not b₁ / b₂ > 0 or ( b₂ > 0 & b₁ > 0 ) or ( b₂ < 0 & b₁ < 0 ) )

proof end;

theorem Th147: :: XREAL_1:147

for b₁, b₂ being real number st b₁ <= b₂ holds
b₁ < b₂ + 1

proof end;

theorem Th148: :: XREAL_1:148

for b₁ being real number holds b₁ - 1 < b₁

proof end;

theorem Th149: :: XREAL_1:149

for b₁, b₂ being real number st b₁ <= b₂ holds
b₁ - 1 < b₂

proof end;

theorem Th150: :: XREAL_1:150

for b₁ being real number st - 1 < b₁ holds
0 < 1 + b₁

proof end;

theorem Th151: :: XREAL_1:151

for b₁ being real number st b₁ < 1 holds
1 - b₁ > 0 by Lemma26;

theorem Th152: :: XREAL_1:152

for b₁, b₂ being real number st 0 <= b₁ & b₁ <= 1 & 0 <= b₂ & b₂ <= 1 & b₁ * b₂ = 1 holds
b₁ = 1

proof end;

theorem Th153: :: XREAL_1:153

for b₁, b₂ being real number st 0 <= b₁ & 1 <= b₂ holds
b₁ <= b₁ * b₂

proof end;

theorem Th154: :: XREAL_1:154

for b₁, b₂ being real number st b₁ <= 0 & b₂ <= 1 holds
b₁ <= b₁ * b₂

proof end;

theorem Th155: :: XREAL_1:155

for b₁, b₂ being real number st 0 <= b₁ & b₂ <= 1 holds
b₁ * b₂ <= b₁

proof end;

theorem Th156: :: XREAL_1:156

for b₁, b₂ being real number st b₁ <= 0 & 1 <= b₂ holds
b₁ * b₂ <= b₁

proof end;

theorem Th157: :: XREAL_1:157

for b₁, b₂ being real number st 0 < b₁ & 1 < b₂ holds
b₁ < b₁ * b₂

proof end;

theorem Th158: :: XREAL_1:158

for b₁, b₂ being real number st b₁ < 0 & b₂ < 1 holds
b₁ < b₁ * b₂

proof end;

theorem Th159: :: XREAL_1:159

for b₁, b₂ being real number st 0 < b₁ & b₂ < 1 holds
b₁ * b₂ < b₁

proof end;

theorem Th160: :: XREAL_1:160

for b₁, b₂ being real number st b₁ < 0 & 1 < b₂ holds
b₁ * b₂ < b₁

proof end;

theorem Th161: :: XREAL_1:161

for b₁, b₂ being real number st 1 <= b₁ & 1 <= b₂ holds
1 <= b₁ * b₂

proof end;

theorem Th162: :: XREAL_1:162

for b₁, b₂ being real number st 0 <= b₁ & b₁ <= 1 & 0 <= b₂ & b₂ <= 1 holds
b₁ * b₂ <= 1

proof end;

theorem Th163: :: XREAL_1:163

for b₁, b₂ being real number st 1 < b₁ & 1 <= b₂ holds
1 < b₁ * b₂

proof end;

theorem Th164: :: XREAL_1:164

for b₁, b₂ being real number st 0 <= b₁ & b₁ < 1 & 0 <= b₂ & b₂ <= 1 holds
b₁ * b₂ < 1

proof end;

theorem Th165: :: XREAL_1:165

for b₁, b₂ being real number st b₁ <= - 1 & b₂ <= - 1 holds
1 <= b₁ * b₂

proof end;

theorem Th166: :: XREAL_1:166

for b₁, b₂ being real number st b₁ < - 1 & b₂ <= - 1 holds
1 < b₁ * b₂

proof end;

theorem Th167: :: XREAL_1:167

for b₁, b₂ being real number st b₁ <= 0 & - 1 <= b₁ & b₂ <= 0 & - 1 <= b₂ holds
b₁ * b₂ <= 1

proof end;

theorem Th168: :: XREAL_1:168

for b₁, b₂ being real number st b₁ <= 0 & - 1 < b₁ & b₂ <= 0 & - 1 <= b₂ holds
b₁ * b₂ < 1

proof end;

theorem Th169: :: XREAL_1:169

for b₁, b₂ being real number st ( for b₃ being real number st 1 < b₃ holds
b₁ <= b₂ * b₃ ) holds
b₁ <= b₂

proof end;

Lemma78: for b₁ being real number st 1 < b₁ holds
b₁ " < 1

proof end;

theorem Th170: :: XREAL_1:170

for b₁, b₂ being real number st ( for b₃ being real number st 0 < b₃ & b₃ < 1 holds
b₁ * b₃ <= b₂ ) holds
b₁ <= b₂

proof end;

Lemma79: for b₁, b₂ being real number st b₁ <= b₂ & 0 <= b₁ holds
b₁ / b₂ <= 1

proof end;

Lemma80: for b₁, b₂ being real number st b₁ <= b₂ & 0 <= b₂ holds
b₁ / b₂ <= 1

proof end;

theorem Th171: :: XREAL_1:171

for b₁, b₂ being real number st ( for b₃ being real number st 0 < b₃ & b₃ < 1 holds
b₁ <= b₃ * b₂ ) holds
b₁ <= 0

proof end;

theorem Th172: :: XREAL_1:172

for b₁, b₂, b₃ being real number st 0 <= b₁ & b₁ <= 1 & 0 <= b₂ & 0 <= b₃ & (b₁ * b₂) + ((1 - b₁) * b₃) = 0 & not ( b₁ = 0 & b₃ = 0 ) & not ( b₁ = 1 & b₂ = 0 ) holds
( b₂ = 0 & b₃ = 0 )

proof end;

theorem Th173: :: XREAL_1:173

for b₁, b₂, b₃ being real number st 0 <= b₁ & b₁ <= 1 & b₂ <= b₃ holds
b₂ <= ((1 - b₁) * b₂) + (b₁ * b₃)

proof end;

theorem Th174: :: XREAL_1:174

for b₁, b₂, b₃ being real number st 0 <= b₁ & b₁ <= 1 & b₂ <= b₃ holds
((1 - b₁) * b₂) + (b₁ * b₃) <= b₃

proof end;

theorem Th175: :: XREAL_1:175

for b₁, b₂, b₃, b₄ being real number st 0 <= b₁ & b₁ <= 1 & b₂ <= b₃ & b₂ <= b₄ holds
b₂ <= ((1 - b₁) * b₃) + (b₁ * b₄)

proof end;

theorem Th176: :: XREAL_1:176

for b₁, b₂, b₃, b₄ being real number st 0 <= b₁ & b₁ <= 1 & b₂ <= b₃ & b₄ <= b₃ holds
((1 - b₁) * b₂) + (b₁ * b₄) <= b₃

proof end;

theorem Th177: :: XREAL_1:177

for b₁, b₂, b₃, b₄ being real number st 0 <= b₁ & b₁ <= 1 & b₂ < b₃ & b₂ < b₄ holds
b₂ < ((1 - b₁) * b₃) + (b₁ * b₄)

proof end;

theorem Th178: :: XREAL_1:178

for b₁, b₂, b₃, b₄ being real number st 0 <= b₁ & b₁ <= 1 & b₂ < b₃ & b₄ < b₃ holds
((1 - b₁) * b₂) + (b₁ * b₄) < b₃

proof end;

theorem Th179: :: XREAL_1:179

for b₁, b₂, b₃, b₄ being real number st 0 < b₁ & b₁ < 1 & b₂ <= b₃ & b₂ < b₄ holds
b₂ < ((1 - b₁) * b₃) + (b₁ * b₄)

proof end;

theorem Th180: :: XREAL_1:180

for b₁, b₂, b₃, b₄ being real number st 0 < b₁ & b₁ < 1 & b₂ < b₃ & b₄ <= b₃ holds
((1 - b₁) * b₂) + (b₁ * b₄) < b₃

proof end;

theorem Th181: :: XREAL_1:181

for b₁, b₂, b₃ being real number st 0 <= b₁ & b₁ <= 1 & b₂ <= ((1 - b₁) * b₂) + (b₁ * b₃) & b₃ < ((1 - b₁) * b₂) + (b₁ * b₃) holds
b₁ = 0

proof end;

theorem Th182: :: XREAL_1:182

for b₁, b₂, b₃ being real number st 0 <= b₁ & b₁ <= 1 & ((1 - b₁) * b₂) + (b₁ * b₃) <= b₂ & ((1 - b₁) * b₂) + (b₁ * b₃) < b₃ holds
b₁ = 0

proof end;

theorem Th183: :: XREAL_1:183

for b₁, b₂ being real number st 0 < b₁ & b₁ <= b₂ holds
1 <= b₂ / b₁

proof end;

theorem Th184: :: XREAL_1:184

for b₁, b₂ being real number st b₁ < 0 & b₂ <= b₁ holds
1 <= b₂ / b₁

proof end;

theorem Th185: :: XREAL_1:185

for b₁, b₂ being real number st 0 <= b₁ & b₁ <= b₂ holds
b₁ / b₂ <= 1 by Lemma79;

theorem Th186: :: XREAL_1:186

for b₁, b₂ being real number st b₁ <= b₂ & b₂ <= 0 holds
b₂ / b₁ <= 1

proof end;

theorem Th187: :: XREAL_1:187

for b₁, b₂ being real number st 0 <= b₁ & b₂ <= b₁ holds
b₂ / b₁ <= 1 by Lemma80;

theorem Th188: :: XREAL_1:188

for b₁, b₂ being real number st b₁ <= 0 & b₁ <= b₂ holds
b₂ / b₁ <= 1

proof end;

theorem Th189: :: XREAL_1:189

for b₁, b₂ being real number st 0 < b₁ & b₁ < b₂ holds
1 < b₂ / b₁

proof end;

theorem Th190: :: XREAL_1:190

for b₁, b₂ being real number st b₁ < 0 & b₂ < b₁ holds
1 < b₂ / b₁

proof end;

theorem Th191: :: XREAL_1:191

for b₁, b₂ being real number st 0 <= b₁ & b₁ < b₂ holds
b₁ / b₂ < 1

proof end;

theorem Th192: :: XREAL_1:192

for b₁, b₂ being real number st b₁ <= 0 & b₂ < b₁ holds
b₁ / b₂ < 1

proof end;

theorem Th193: :: XREAL_1:193

for b₁, b₂ being real number st 0 < b₁ & b₂ < b₁ holds
b₂ / b₁ < 1

proof end;

theorem Th194: :: XREAL_1:194

for b₁, b₂ being real number st b₁ < 0 & b₁ < b₂ holds
b₂ / b₁ < 1

proof end;

theorem Th195: :: XREAL_1:195

for b₁, b₂ being real number st 0 <= b₁ & - b₁ <= b₂ holds
- 1 <= b₂ / b₁

proof end;

theorem Th196: :: XREAL_1:196

for b₁, b₂ being real number st 0 <= b₁ & - b₂ <= b₁ holds
- 1 <= b₂ / b₁

proof end;

theorem Th197: :: XREAL_1:197

for b₁, b₂ being real number st b₁ <= 0 & b₂ <= - b₁ holds
- 1 <= b₂ / b₁

proof end;

theorem Th198: :: XREAL_1:198

for b₁, b₂ being real number st b₁ <= 0 & b₁ <= - b₂ holds
- 1 <= b₂ / b₁

proof end;

theorem Th199: :: XREAL_1:199

for b₁, b₂ being real number st 0 < b₁ & - b₁ < b₂ holds
- 1 < b₂ / b₁

proof end;

theorem Th200: :: XREAL_1:200

for b₁, b₂ being real number st 0 < b₁ & - b₂ < b₁ holds
- 1 < b₂ / b₁

proof end;

theorem Th201: :: XREAL_1:201

for b₁, b₂ being real number st b₁ < 0 & b₂ < - b₁ holds
- 1 < b₂ / b₁

proof end;

theorem Th202: :: XREAL_1:202

for b₁, b₂ being real number st b₁ < 0 & b₁ < - b₂ holds
- 1 < b₂ / b₁

proof end;

theorem Th203: :: XREAL_1:203

for b₁, b₂ being real number st 0 < b₁ & b₂ <= - b₁ holds
b₂ / b₁ <= - 1

proof end;

theorem Th204: :: XREAL_1:204

for b₁, b₂ being real number st 0 < b₁ & b₁ <= - b₂ holds
b₂ / b₁ <= - 1

proof end;

theorem Th205: :: XREAL_1:205

for b₁, b₂ being real number st b₁ < 0 & - b₁ <= b₂ holds
b₂ / b₁ <= - 1

proof end;

theorem Th206: :: XREAL_1:206

for b₁, b₂ being real number st b₁ < 0 & - b₂ <= b₁ holds
b₂ / b₁ <= - 1

proof end;

theorem Th207: :: XREAL_1:207

for b₁, b₂ being real number st 0 < b₁ & b₂ < - b₁ holds
b₂ / b₁ < - 1

proof end;

theorem Th208: :: XREAL_1:208

for b₁, b₂ being real number st 0 < b₁ & b₁ < - b₂ holds
b₂ / b₁ < - 1

proof end;

theorem Th209: :: XREAL_1:209

for b₁, b₂ being real number st b₁ < 0 & - b₁ < b₂ holds
b₂ / b₁ < - 1

proof end;

theorem Th210: :: XREAL_1:210

for b₁, b₂ being real number st b₁ < 0 & - b₂ < b₁ holds
b₂ / b₁ < - 1

proof end;

theorem Th211: :: XREAL_1:211

for b₁, b₂ being real number st ( for b₃ being real number st 0 < b₃ & b₃ < 1 holds
b₁ <= b₂ / b₃ ) holds
b₁ <= b₂

proof end;

theorem Th212: :: XREAL_1:212

for b₁, b₂ being real number st ( for b₃ being real number st 1 < b₃ holds
b₁ / b₃ <= b₂ ) holds
b₁ <= b₂

proof end;

theorem Th213: :: XREAL_1:213

for b₁ being real number st 1 <= b₁ holds
b₁ " <= 1

proof end;

theorem Th214: :: XREAL_1:214

for b₁ being real number st 1 < b₁ holds
b₁ " < 1 by Lemma78;

theorem Th215: :: XREAL_1:215

for b₁ being real number st b₁ <= - 1 holds
- 1 <= b₁ "

proof end;

theorem Th216: :: XREAL_1:216

for b₁ being real number st b₁ < - 1 holds
- 1 < b₁ "

proof end;

theorem Th217: :: XREAL_1:217

for b₁ being real number st 0 < b₁ holds
0 < b₁ / 2 by Lemma41;

theorem Th218: :: XREAL_1:218

for b₁ being real number st 0 < b₁ holds
b₁ / 2 < b₁ by Lemma42;

theorem Th219: :: XREAL_1:219

for b₁ being real number st b₁ <= 1 / 2 holds
(2 * b₁) - 1 <= 0

proof end;

theorem Th220: :: XREAL_1:220

for b₁ being real number st b₁ <= 1 / 2 holds
0 <= 1 - (2 * b₁)

proof end;

theorem Th221: :: XREAL_1:221

for b₁ being real number st b₁ >= 1 / 2 holds
(2 * b₁) - 1 >= 0

proof end;

theorem Th222: :: XREAL_1:222

for b₁ being real number st b₁ >= 1 / 2 holds
0 >= 1 - (2 * b₁)

proof end;

theorem Th223: :: XREAL_1:223

for b₁ being real number st 0 < b₁ holds
b₁ / 3 < b₁

proof end;

theorem Th224: :: XREAL_1:224

for b₁ being real number st 0 < b₁ holds
0 < b₁ / 3

proof end;

theorem Th225: :: XREAL_1:225

for b₁ being real number st 0 < b₁ holds
b₁ / 4 < b₁

proof end;

theorem Th226: :: XREAL_1:226

for b₁ being real number st 0 < b₁ holds
0 < b₁ / 4

proof end;

theorem Th227: :: XREAL_1:227

for b₁, b₂ being real number st b₂ <> 0 holds
ex b₃ being real number st b₁ = b₂ / b₃

proof end;