:: JORDAN5A semantic presentation

theorem Th1: :: JORDAN5A:1

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄ being Subset of (TOP-REAL b₁) st b₄ is_an_arc_of b₂,b₃ holds
b₄ is compact

proof end;

Lemma2: for b₁ being Nat holds
( the carrier of (Euclid b₁) = REAL b₁ & the carrier of (TOP-REAL b₁) = REAL b₁ )

proof end;

theorem Th2: :: JORDAN5A:2

for b₁ being real number holds
( ( 0 <= b₁ & b₁ <= 1 ) iff b₁ in the carrier of I[01] )

proof end;

theorem Th3: :: JORDAN5A:3

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄, b₅ being real number holds
( not ((1 - b₄) * b₂) + (b₄ * b₃) = ((1 - b₅) * b₂) + (b₅ * b₃) or b₄ = b₅ or b₂ = b₃ )

proof end;

theorem Th4: :: JORDAN5A:4

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) st b₂ <> b₃ holds
ex b₄ being Function of I[01] ,((TOP-REAL b₁) | (LSeg b₂,b₃)) st
( ( for b₅ being Real st b₅ in [.0,1.] holds
b₄ . b₅ = ((1 - b₅) * b₂) + (b₅ * b₃) ) & b₄ is_homeomorphism & b₄ . 0 = b₂ & b₄ . 1 = b₃ )

proof end;

Lemma6: for b₁ being Nat holds TOP-REAL b₁ is arcwise_connected

proof end;

registration

let c₁ be Nat;
cluster TOP-REAL a₁ -> arcwise_connected ;
coherence by Lemma6;

end;

registration

let c₁ be Nat;
cluster non empty strict compact SubSpace of TOP-REAL a₁;
existence

proof end;

end;

theorem Th5: :: JORDAN5A:5

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being Path of b₁,b₂
for b₄ being non empty compact SubSpace of TOP-REAL 2
for b₅ being Function of I[01] ,b₄ st b₃ is one-to-one & b₅ = b₃ & [#] b₄ = rng b₃ holds
b₅ is_homeomorphism

proof end;

Lemma7: for b₁ being Subset of REAL st b₁ is open holds
b₁ in Family_open_set RealSpace

proof end;

Lemma8: for b₁ being Subset of REAL st b₁ in Family_open_set RealSpace holds
b₁ is open

proof end;

theorem Th6: :: JORDAN5A:6

for b₁ being Subset of REAL holds
( b₁ in Family_open_set RealSpace iff b₁ is open ) by Lemma7, Lemma8;

theorem Th7: :: JORDAN5A:7

for b₁ being Function of R^1 ,R^1
for b₂ being Point of R^1
for b₃ being PartFunc of REAL , REAL
for b₄ being Real st b₁ is_continuous_at b₂ & b₁ = b₃ & b₂ = b₄ holds
b₃ is_continuous_in b₄

proof end;

theorem Th8: :: JORDAN5A:8

for b₁ being continuous Function of R^1 ,R^1
for b₂ being PartFunc of REAL , REAL st b₁ = b₂ holds
b₂ is_continuous_on REAL

proof end;

Lemma11: for b₁ being one-to-one continuous Function of R^1 ,R^1
for b₂ being PartFunc of REAL , REAL holds
( not b₁ = b₂ or b₂ is_increasing_on [.0,1.] or b₂ is_decreasing_on [.0,1.] )

proof end;

theorem Th9: :: JORDAN5A:9

for b₁ being one-to-one continuous Function of R^1 ,R^1 holds
( for b₂, b₃ being Point of I[01]
for b₄, b₅, b₆, b₇ being Real st b₂ = b₄ & b₃ = b₅ & b₄ < b₅ & b₆ = b₁ . b₂ & b₇ = b₁ . b₃ holds
b₆ < b₇ or for b₂, b₃ being Point of I[01]
for b₄, b₅, b₆, b₇ being Real st b₂ = b₄ & b₃ = b₅ & b₄ < b₅ & b₆ = b₁ . b₂ & b₇ = b₁ . b₃ holds
b₆ > b₇ )

proof end;

theorem Th10: :: JORDAN5A:10

for b₁, b₂, b₃, b₄ being Real
for b₅ being Element of (Closed-Interval-MSpace b₃,b₄) st b₃ <= b₄ & b₅ = b₁ & b₂ > 0 & ].(b₁ - b₂),(b₁ + b₂).[ c= [.b₃,b₄.] holds
].(b₁ - b₂),(b₁ + b₂).[ = Ball b₅,b₂

proof end;

theorem Th11: :: JORDAN5A:11

for b₁, b₂ being Real
for b₃ being Subset of REAL st b₁ < b₂ & not b₁ in b₃ & not b₂ in b₃ & b₃ in Family_open_set (Closed-Interval-MSpace b₁,b₂) holds
b₃ is open

proof end;

theorem Th12: :: JORDAN5A:12

for b₁ being open Subset of REAL
for b₂, b₃ being Real st b₁ c= [.b₂,b₃.] holds
( not b₂ in b₁ & not b₃ in b₁ )

proof end;

theorem Th13: :: JORDAN5A:13

for b₁, b₂ being Real
for b₃ being Subset of REAL
for b₄ being Subset of (Closed-Interval-MSpace b₁,b₂) st b₁ <= b₂ & b₄ = b₃ & b₃ is open holds
b₄ in Family_open_set (Closed-Interval-MSpace b₁,b₂)

proof end;

Lemma16: for b₁, b₂, b₃ being real number st b₁ <= b₂ holds
( b₃ in the carrier of (Closed-Interval-TSpace b₁,b₂) iff ( b₁ <= b₃ & b₃ <= b₂ ) )

proof end;

Lemma17: for b₁, b₂, b₃, b₄ being Real
for b₅ being Function of (Closed-Interval-TSpace b₁,b₂),(Closed-Interval-TSpace b₃,b₄)
for b₆ being Point of (Closed-Interval-TSpace b₁,b₂)
for b₇ being PartFunc of REAL , REAL
for b₈ being Real st b₁ < b₂ & b₃ < b₄ & b₅ is_continuous_at b₆ & b₆ <> b₁ & b₆ <> b₂ & b₅ . b₁ = b₃ & b₅ . b₂ = b₄ & b₅ is one-to-one & b₅ = b₇ & b₆ = b₈ holds
b₇ is_continuous_in b₈

proof end;

theorem Th14: :: JORDAN5A:14

for b₁, b₂, b₃, b₄, b₅ being Real
for b₆ being Function of (Closed-Interval-TSpace b₁,b₂),(Closed-Interval-TSpace b₃,b₄)
for b₇ being Point of (Closed-Interval-TSpace b₁,b₂)
for b₈ being PartFunc of REAL , REAL st b₁ < b₂ & b₃ < b₄ & b₆ is_continuous_at b₇ & b₆ . b₁ = b₃ & b₆ . b₂ = b₄ & b₆ is one-to-one & b₆ = b₈ & b₇ = b₅ holds
b₈ | [.b₁,b₂.] is_continuous_in b₅

proof end;

theorem Th15: :: JORDAN5A:15

for b₁, b₂, b₃, b₄ being Real
for b₅ being Function of (Closed-Interval-TSpace b₁,b₂),(Closed-Interval-TSpace b₃,b₄)
for b₆ being PartFunc of REAL , REAL st b₅ is continuous & b₅ is one-to-one & b₁ < b₂ & b₃ < b₄ & b₅ = b₆ & b₅ . b₁ = b₃ & b₅ . b₂ = b₄ holds
b₆ is_continuous_on [.b₁,b₂.]

proof end;

theorem Th16: :: JORDAN5A:16

for b₁, b₂, b₃, b₄ being Real
for b₅ being Function of (Closed-Interval-TSpace b₁,b₂),(Closed-Interval-TSpace b₃,b₄) st b₁ < b₂ & b₃ < b₄ & b₅ is continuous & b₅ is one-to-one & b₅ . b₁ = b₃ & b₅ . b₂ = b₄ holds
for b₆, b₇ being Point of (Closed-Interval-TSpace b₁,b₂)
for b₈, b₉, b₁₀, b₁₁ being Real st b₆ = b₈ & b₇ = b₉ & b₈ < b₉ & b₁₀ = b₅ . b₆ & b₁₁ = b₅ . b₇ holds
b₁₀ < b₁₁

proof end;

theorem Th17: :: JORDAN5A:17

for b₁ being one-to-one continuous Function of I[01] ,I[01] st b₁ . 0 = 0 & b₁ . 1 = 1 holds
for b₂, b₃ being Point of I[01]
for b₄, b₅, b₆, b₇ being Real st b₂ = b₄ & b₃ = b₅ & b₄ < b₅ & b₆ = b₁ . b₂ & b₇ = b₁ . b₃ holds
b₆ < b₇ by Th16, TOPMETR:27;

theorem Th18: :: JORDAN5A:18

for b₁, b₂, b₃, b₄ being Real
for b₅ being Function of (Closed-Interval-TSpace b₁,b₂),(Closed-Interval-TSpace b₃,b₄)
for b₆ being non empty Subset of (Closed-Interval-TSpace b₁,b₂)
for b₇, b₈ being Subset of R^1 st b₁ < b₂ & b₃ < b₄ & b₇ = b₆ & b₅ is continuous & b₅ is one-to-one & b₇ is compact & b₅ . b₁ = b₃ & b₅ . b₂ = b₄ & b₅ .: b₆ = b₈ holds
b₅ . (lower_bound ([#] b₇)) = lower_bound ([#] b₈)

proof end;

theorem Th19: :: JORDAN5A:19

for b₁, b₂, b₃, b₄ being Real
for b₅ being Function of (Closed-Interval-TSpace b₁,b₂),(Closed-Interval-TSpace b₃,b₄)
for b₆, b₇ being non empty Subset of (Closed-Interval-TSpace b₁,b₂)
for b₈, b₉ being Subset of R^1 st b₁ < b₂ & b₃ < b₄ & b₈ = b₆ & b₉ = b₇ & b₅ is continuous & b₅ is one-to-one & b₈ is compact & b₅ . b₁ = b₃ & b₅ . b₂ = b₄ & b₅ .: b₆ = b₇ holds
b₅ . (upper_bound ([#] b₈)) = upper_bound ([#] b₉)

proof end;

theorem Th20: :: JORDAN5A:20

for b₁, b₂ being real number st b₁ <= b₂ holds
( lower_bound [.b₁,b₂.] = b₁ & upper_bound [.b₁,b₂.] = b₂ )

proof end;

theorem Th21: :: JORDAN5A:21

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Real
for b₉ being Function of (Closed-Interval-TSpace b₁,b₂),(Closed-Interval-TSpace b₃,b₄) st b₁ < b₂ & b₃ < b₄ & b₅ < b₆ & b₁ <= b₅ & b₆ <= b₂ & b₉ is_homeomorphism & b₉ . b₁ = b₃ & b₉ . b₂ = b₄ & b₇ = b₉ . b₅ & b₈ = b₉ . b₆ holds
b₉ .: [.b₅,b₆.] = [.b₇,b₈.]

proof end;

theorem Th22: :: JORDAN5A:22

for b₁, b₂ being Subset of (TOP-REAL 2)
for b₃, b₄ being Point of (TOP-REAL 2) st b₁ meets b₂ & b₁ /\ b₂ is closed & b₁ is_an_arc_of b₃,b₄ holds
ex b₅ being Point of (TOP-REAL 2) st
( b₅ in b₁ /\ b₂ & ex b₆ being Function of I[01] ,((TOP-REAL 2) | b₁)ex b₇ being Real st
( b₆ is_homeomorphism & b₆ . 0 = b₃ & b₆ . 1 = b₄ & b₆ . b₇ = b₅ & 0 <= b₇ & b₇ <= 1 & ( for b₈ being Real st 0 <= b₈ & b₈ < b₇ holds
not b₆ . b₈ in b₂ ) ) )

proof end;

theorem Th23: :: JORDAN5A:23

for b₁, b₂ being Subset of (TOP-REAL 2)
for b₃, b₄ being Point of (TOP-REAL 2) st b₁ meets b₂ & b₁ /\ b₂ is closed & b₁ is_an_arc_of b₃,b₄ holds
ex b₅ being Point of (TOP-REAL 2) st
( b₅ in b₁ /\ b₂ & ex b₆ being Function of I[01] ,((TOP-REAL 2) | b₁)ex b₇ being Real st
( b₆ is_homeomorphism & b₆ . 0 = b₃ & b₆ . 1 = b₄ & b₆ . b₇ = b₅ & 0 <= b₇ & b₇ <= 1 & ( for b₈ being Real st 1 >= b₈ & b₈ > b₇ holds
not b₆ . b₈ in b₂ ) ) )

proof end;