:: REAL semantic presentation

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

proof end;

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

proof end;

theorem Th1: :: REAL:1

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

proof end;

theorem Th2: :: REAL:2

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

proof end;

theorem Th3: :: REAL:3

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

proof end;

theorem Th4: :: REAL:4

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

proof end;

theorem Th5: :: REAL:5

for b₁, b₂ being real number st b₁ <= b₂ & not b₂ is empty & not b₁ is negative holds
b₂ is positive

proof end;

theorem Th6: :: REAL:6

for b₁, b₂ being real number st b₁ <= b₂ & not b₁ is empty & not b₂ is positive holds
b₁ is negative

proof end;

theorem Th7: :: REAL:7

for b₁, b₂ being real number st not b₁ <= b₂ & not b₁ is positive holds
b₂ is negative

proof end;

theorem Th8: :: REAL:8

for b₁, b₂ being real number st not b₁ <= b₂ & not b₂ is negative holds
b₁ is positive

proof end;