:: TOPREAL5 semantic presentation

Lemma1: for b₁, b₂, b₃ being real number holds
( b₃ in [.b₁,b₂.] iff ( b₁ <= b₃ & b₃ <= b₂ ) )
by RCOMP_1:48;

Lemma2: for b₁, b₂, b₃ being non empty TopSpace
for b₄ being continuous Function of b₁,b₂
for b₅ being continuous Function of b₂,b₃ holds b₅ * b₄ is continuous Function of b₁,b₃
;

theorem Th1: :: TOPREAL5:1

canceled;

theorem Th2: :: TOPREAL5:2

canceled;

theorem Th3: :: TOPREAL5:3

canceled;

theorem Th4: :: TOPREAL5:4

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being Subset of b₁ st b₃ is open & b₄ is open & b₃ meets b₂ & b₄ meets b₂ & b₂ c= b₃ \/ b₄ & b₃ misses b₄ holds
not b₂ is connected

proof end;

theorem Th5: :: TOPREAL5:5

for b₁, b₂ being non empty TopSpace
for b₃ being continuous Function of b₁,b₂
for b₄ being Subset of b₁ st b₄ is connected holds
b₃ .: b₄ is connected

proof end;

theorem Th6: :: TOPREAL5:6

for b₁, b₂ being real number st b₁ <= b₂ holds
[#] (Closed-Interval-TSpace b₁,b₂) is connected

proof end;

Lemma6: for b₁ being Subset of R^1
for b₂ being real number st b₁ = { b₃ where B is Element of REAL : b₂ < b₃ } holds
b₁ is open
by JORDAN2B:31;

Lemma7: for b₁ being Subset of R^1
for b₂ being real number st b₁ = { b₃ where B is Element of REAL : b₂ > b₃ } holds
b₁ is open
by JORDAN2B:30;

theorem Th7: :: TOPREAL5:7

canceled;

theorem Th8: :: TOPREAL5:8

canceled;

theorem Th9: :: TOPREAL5:9

for b₁ being Subset of R^1
for b₂ being real number st not b₂ in b₁ & ex b₃, b₄ being real number st
( b₃ in b₁ & b₄ in b₁ & b₃ < b₂ & b₂ < b₄ ) holds
not b₁ is connected

proof end;

theorem Th10: :: TOPREAL5:10

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁
for b₄, b₅, b₆ being Real
for b₇ being continuous Function of b₁,R^1 st b₁ is connected & b₇ . b₂ = b₄ & b₇ . b₃ = b₅ & b₄ <= b₆ & b₆ <= b₅ holds
ex b₈ being Point of b₁ st b₇ . b₈ = b₆

proof end;

theorem Th11: :: TOPREAL5:11

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁
for b₄ being Subset of b₁
for b₅, b₆, b₇ being Real
for b₈ being continuous Function of b₁,R^1 st b₄ is connected & b₈ . b₂ = b₅ & b₈ . b₃ = b₆ & b₅ <= b₇ & b₇ <= b₆ & b₂ in b₄ & b₃ in b₄ holds
ex b₉ being Point of b₁ st
( b₉ in b₄ & b₈ . b₉ = b₇ )

proof end;

theorem Th12: :: TOPREAL5:12

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ holds
for b₅ being continuous Function of (Closed-Interval-TSpace b₁,b₂),R^1
for b₆ being real number st b₅ . b₁ = b₃ & b₅ . b₂ = b₄ & b₃ < b₆ & b₆ < b₄ holds
ex b₇ being Element of REAL st
( b₅ . b₇ = b₆ & b₁ < b₇ & b₇ < b₂ )

proof end;

theorem Th13: :: TOPREAL5:13

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ holds
for b₅ being continuous Function of (Closed-Interval-TSpace b₁,b₂),R^1
for b₆ being real number st b₅ . b₁ = b₃ & b₅ . b₂ = b₄ & b₃ > b₆ & b₆ > b₄ holds
ex b₇ being Element of REAL st
( b₅ . b₇ = b₆ & b₁ < b₇ & b₇ < b₂ )

proof end;

theorem Th14: :: TOPREAL5:14

for b₁, b₂ being real number
for b₃ being continuous Function of (Closed-Interval-TSpace b₁,b₂),R^1
for b₄, b₅ being real number st b₁ < b₂ & b₄ * b₅ < 0 & b₄ = b₃ . b₁ & b₅ = b₃ . b₂ holds
ex b₆ being Element of REAL st
( b₃ . b₆ = 0 & b₁ < b₆ & b₆ < b₂ )

proof end;

theorem Th15: :: TOPREAL5:15

for b₁ being Function of I[01] ,R^1
for b₂, b₃ being real number st b₁ is continuous & b₁ . 0 <> b₁ . 1 & b₂ = b₁ . 0 & b₃ = b₁ . 1 holds
ex b₄ being Element of REAL st
( 0 < b₄ & b₄ < 1 & b₁ . b₄ = (b₂ + b₃) / 2 )

proof end;

theorem Th16: :: TOPREAL5:16

for b₁ being Function of (TOP-REAL 2),R^1 st b₁ = proj1 holds
b₁ is continuous

proof end;

theorem Th17: :: TOPREAL5:17

for b₁ being Function of (TOP-REAL 2),R^1 st b₁ = proj2 holds
b₁ is continuous

proof end;

theorem Th18: :: TOPREAL5:18

for b₁ being non empty Subset of (TOP-REAL 2)
for b₂ being Function of I[01] ,((TOP-REAL 2) | b₁) st b₂ is continuous holds
ex b₃ being Function of I[01] ,R^1 st
( b₃ is continuous & ( for b₄ being Element of REAL
for b₅ being Point of (TOP-REAL 2) st b₄ in the carrier of I[01] & b₅ = b₂ . b₄ holds
b₅ `1 = b₃ . b₄ ) )

proof end;

theorem Th19: :: TOPREAL5:19

proof end;

theorem Th20: :: TOPREAL5:20

for b₁ being non empty Subset of (TOP-REAL 2) st b₁ is being_simple_closed_curve holds
for b₂ being Element of REAL ex b₃ being Point of (TOP-REAL 2) st
( b₃ in b₁ & not b₃ `2 = b₂ )

proof end;

theorem Th21: :: TOPREAL5:21

for b₁ being non empty Subset of (TOP-REAL 2) st b₁ is being_simple_closed_curve holds
for b₂ being Element of REAL ex b₃ being Point of (TOP-REAL 2) st
( b₃ in b₁ & not b₃ `1 = b₂ )

proof end;

theorem Th22: :: TOPREAL5:22

for b₁ being non empty compact Subset of (TOP-REAL 2) st b₁ is_simple_closed_curve holds
N-bound b₁ > S-bound b₁

proof end;

theorem Th23: :: TOPREAL5:23

for b₁ being non empty compact Subset of (TOP-REAL 2) st b₁ is_simple_closed_curve holds
E-bound b₁ > W-bound b₁

proof end;

theorem Th24: :: TOPREAL5:24

for b₁ being non empty compact Subset of (TOP-REAL 2) st b₁ is_simple_closed_curve holds
S-min b₁ <> N-max b₁

proof end;

theorem Th25: :: TOPREAL5:25

for b₁ being non empty compact Subset of (TOP-REAL 2) st b₁ is_simple_closed_curve holds
W-min b₁ <> E-max b₁

proof end;