:: JORDAN5C semantic presentation

Lemma1: for b₁ being Real st 0 <= b₁ & b₁ <= 1 holds
( 0 <= 1 - b₁ & 1 - b₁ <= 1 )

proof end;

theorem Th1: :: JORDAN5C:1

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

proof end;

definition

let c₁, c₂ be Subset of (TOP-REAL 2);
let c₃, c₄ be Point of (TOP-REAL 2);
assume E3: ( c₁ meets c₂ & c₁ /\ c₂ is closed & c₁ is_an_arc_of c₃,c₄ ) ;
func First_Point c₁,c₃,c₄,c₂ -> Point of (TOP-REAL 2) means :Def1: :: JORDAN5C:def 1
( a₅ in a₁ /\ a₂ & ( for b₁ being Function of I[01] ,((TOP-REAL 2) | a₁)
for b₂ being Real st b₁ is_homeomorphism & b₁ . 0 = a₃ & b₁ . 1 = a₄ & b₁ . b₂ = a₅ & 0 <= b₂ & b₂ <= 1 holds
for b₃ being Real st 0 <= b₃ & b₃ < b₂ holds
not b₁ . b₃ in a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines First_Point JORDAN5C:def 1 :

theorem Th2: :: JORDAN5C:2

for b₁, b₂ being Subset of (TOP-REAL 2)
for b₃, b₄, b₅ being Point of (TOP-REAL 2) st b₃ in b₁ & b₁ is_an_arc_of b₄,b₅ & b₂ = {b₃} holds
First_Point b₁,b₄,b₅,b₂ = b₃

proof end;

theorem Th3: :: JORDAN5C:3

for b₁, b₂ being Subset of (TOP-REAL 2)
for b₃, b₄ being Point of (TOP-REAL 2) st b₃ in b₂ & b₁ /\ b₂ is closed & b₁ is_an_arc_of b₃,b₄ holds
First_Point b₁,b₃,b₄,b₂ = b₃

proof end;

theorem Th4: :: JORDAN5C:4

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

proof end;

definition

let c₁, c₂ be Subset of (TOP-REAL 2);
let c₃, c₄ be Point of (TOP-REAL 2);
assume E6: ( c₁ meets c₂ & c₁ /\ c₂ is closed & c₁ is_an_arc_of c₃,c₄ ) ;
func Last_Point c₁,c₃,c₄,c₂ -> Point of (TOP-REAL 2) means :Def2: :: JORDAN5C:def 2
( a₅ in a₁ /\ a₂ & ( for b₁ being Function of I[01] ,((TOP-REAL 2) | a₁)
for b₂ being Real st b₁ is_homeomorphism & b₁ . 0 = a₃ & b₁ . 1 = a₄ & b₁ . b₂ = a₅ & 0 <= b₂ & b₂ <= 1 holds
for b₃ being Real st 1 >= b₃ & b₃ > b₂ holds
not b₁ . b₃ in a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Last_Point JORDAN5C:def 2 :

theorem Th5: :: JORDAN5C:5

for b₁, b₂ being Subset of (TOP-REAL 2)
for b₃, b₄, b₅ being Point of (TOP-REAL 2) st b₃ in b₁ & b₁ is_an_arc_of b₄,b₅ & b₂ = {b₃} holds
Last_Point b₁,b₄,b₅,b₂ = b₃

proof end;

theorem Th6: :: JORDAN5C:6

for b₁, b₂ being Subset of (TOP-REAL 2)
for b₃, b₄ being Point of (TOP-REAL 2) st b₄ in b₂ & b₁ /\ b₂ is closed & b₁ is_an_arc_of b₃,b₄ holds
Last_Point b₁,b₃,b₄,b₂ = b₄

proof end;

theorem Th7: :: JORDAN5C:7

for b₁, b₂ being Subset of (TOP-REAL 2)
for b₃, b₄ being Point of (TOP-REAL 2) st b₁ c= b₂ & b₁ is closed & b₁ is_an_arc_of b₃,b₄ holds
( First_Point b₁,b₃,b₄,b₂ = b₃ & Last_Point b₁,b₃,b₄,b₂ = b₄ )

proof end;

definition

let c₁ be Subset of (TOP-REAL 2);
let c₂, c₃, c₄, c₅ be Point of (TOP-REAL 2);
pred LE c₄,c₅,c₁,c₂,c₃ means :Def3: :: JORDAN5C:def 3
( a₄ in a₁ & a₅ in a₁ & ( for b₁ being Function of I[01] ,((TOP-REAL 2) | a₁)
for b₂, b₃ being Real st b₁ is_homeomorphism & b₁ . 0 = a₂ & b₁ . 1 = a₃ & b₁ . b₂ = a₄ & 0 <= b₂ & b₂ <= 1 & b₁ . b₃ = a₅ & 0 <= b₃ & b₃ <= 1 holds
b₂ <= b₃ ) );

end;

:: deftheorem Def3 defines LE JORDAN5C:def 3 :

theorem Th8: :: JORDAN5C:8

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

proof end;

theorem Th9: :: JORDAN5C:9

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₄ in b₁ holds
LE b₄,b₄,b₁,b₂,b₃

proof end;

theorem Th10: :: JORDAN5C:10

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₂,b₃ & b₄ in b₁ holds
( LE b₂,b₄,b₁,b₂,b₃ & LE b₄,b₃,b₁,b₂,b₃ )

proof end;

theorem Th11: :: JORDAN5C:11

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₂,b₃ holds
LE b₂,b₃,b₁,b₂,b₃

proof end;

theorem Th12: :: JORDAN5C:12

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₂,b₃ & LE b₄,b₅,b₁,b₂,b₃ & LE b₅,b₄,b₁,b₂,b₃ holds
b₄ = b₅

proof end;

theorem Th13: :: JORDAN5C:13

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄, b₅, b₆ being Point of (TOP-REAL 2) st LE b₄,b₅,b₁,b₂,b₃ & LE b₅,b₆,b₁,b₂,b₃ holds
LE b₄,b₆,b₁,b₂,b₃

proof end;

theorem Th14: :: JORDAN5C:14

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₂,b₃ & b₄ in b₁ & b₅ in b₁ & b₄ <> b₅ & not ( LE b₄,b₅,b₁,b₂,b₃ & not LE b₅,b₄,b₁,b₂,b₃ ) holds
( LE b₅,b₄,b₁,b₂,b₃ & not LE b₄,b₅,b₁,b₂,b₃ )

proof end;

theorem Th15: :: JORDAN5C:15

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₁ is_S-Seq & (L~ b₁) /\ b₂ is closed & b₃ in L~ b₁ & b₃ in b₂ holds
LE First_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂,b₃, L~ b₁,b₁ /. 1,b₁ /. (len b₁)

proof end;

theorem Th16: :: JORDAN5C:16

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₁ is_S-Seq & (L~ b₁) /\ b₂ is closed & b₃ in L~ b₁ & b₃ in b₂ holds
LE b₃, Last_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂, L~ b₁,b₁ /. 1,b₁ /. (len b₁)

proof end;

theorem Th17: :: JORDAN5C:17

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₃ <> b₄ & LE b₁,b₂, LSeg b₃,b₄,b₃,b₄ holds
LE b₁,b₂,b₃,b₄

proof end;

theorem Th18: :: JORDAN5C:18

for b₁, b₂ being Subset of (TOP-REAL 2)
for b₃, b₄ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₃,b₄ & b₁ meets b₂ & b₁ /\ b₂ is closed holds
( First_Point b₁,b₃,b₄,b₂ = Last_Point b₁,b₄,b₃,b₂ & Last_Point b₁,b₃,b₄,b₂ = First_Point b₁,b₄,b₃,b₂ )

proof end;

theorem Th19: :: JORDAN5C:19

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Nat st L~ b₁ meets b₂ & b₂ is closed & b₁ is_S-Seq & 1 <= b₃ & b₃ + 1 <= len b₁ & First_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂ in LSeg b₁,b₃ holds
First_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂ = First_Point (LSeg b₁,b₃),(b₁ /. b₃),(b₁ /. (b₃ + 1)),b₂

proof end;

theorem Th20: :: JORDAN5C:20

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Nat st L~ b₁ meets b₂ & b₂ is closed & b₁ is_S-Seq & 1 <= b₃ & b₃ + 1 <= len b₁ & Last_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂ in LSeg b₁,b₃ holds
Last_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂ = Last_Point (LSeg b₁,b₃),(b₁ /. b₃),(b₁ /. (b₃ + 1)),b₂

proof end;

theorem Th21: :: JORDAN5C:21

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st 1 <= b₂ & b₂ + 1 <= len b₁ & b₁ is_S-Seq & First_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),(LSeg b₁,b₂) in LSeg b₁,b₂ holds
First_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),(LSeg b₁,b₂) = b₁ /. b₂

proof end;

theorem Th22: :: JORDAN5C:22

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st 1 <= b₂ & b₂ + 1 <= len b₁ & b₁ is_S-Seq & Last_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),(LSeg b₁,b₂) in LSeg b₁,b₂ holds
Last_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),(LSeg b₁,b₂) = b₁ /. (b₂ + 1)

proof end;

theorem Th23: :: JORDAN5C:23

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st b₁ is_S-Seq & 1 <= b₂ & b₂ + 1 <= len b₁ holds
LE b₁ /. b₂,b₁ /. (b₂ + 1), L~ b₁,b₁ /. 1,b₁ /. (len b₁)

proof end;

theorem Th24: :: JORDAN5C:24

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being Nat st b₁ is_S-Seq & 1 <= b₂ & b₂ <= b₃ & b₃ <= len b₁ holds
LE b₁ /. b₂,b₁ /. b₃, L~ b₁,b₁ /. 1,b₁ /. (len b₁)

proof end;

Lemma22: for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2)
for b₄ being Nat st LSeg b₁,b₄ meets b₂ & b₁ is_S-Seq & b₂ is closed & 1 <= b₄ & b₄ + 1 <= len b₁ & b₃ in LSeg b₁,b₄ & b₃ in b₂ holds
LE First_Point (LSeg b₁,b₄),(b₁ /. b₄),(b₁ /. (b₄ + 1)),b₂,b₃,b₁ /. b₄,b₁ /. (b₄ + 1)

proof end;

Lemma23: for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2)
for b₄ being Nat st L~ b₁ meets b₂ & b₁ is_S-Seq & b₂ is closed & First_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂ in LSeg b₁,b₄ & 1 <= b₄ & b₄ + 1 <= len b₁ & b₃ in LSeg b₁,b₄ & b₃ in b₂ holds
LE First_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂,b₃,b₁ /. b₄,b₁ /. (b₄ + 1)

proof end;

Lemma24: for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2)
for b₄ being Nat st LSeg b₁,b₄ meets b₂ & b₁ is_S-Seq & b₂ is closed & 1 <= b₄ & b₄ + 1 <= len b₁ & b₃ in LSeg b₁,b₄ & b₃ in b₂ holds
LE b₃, Last_Point (LSeg b₁,b₄),(b₁ /. b₄),(b₁ /. (b₄ + 1)),b₂,b₁ /. b₄,b₁ /. (b₄ + 1)

proof end;

Lemma25: for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2)
for b₄ being Nat st L~ b₁ meets b₂ & b₁ is_S-Seq & b₂ is closed & Last_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂ in LSeg b₁,b₄ & 1 <= b₄ & b₄ + 1 <= len b₁ & b₃ in LSeg b₁,b₄ & b₃ in b₂ holds
LE b₃, Last_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂,b₁ /. b₄,b₁ /. (b₄ + 1)

proof end;

theorem Th25: :: JORDAN5C:25

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2)
for b₃ being Nat st b₁ is_S-Seq & 1 <= b₃ & b₃ + 1 <= len b₁ & b₂ in LSeg b₁,b₃ holds
LE b₁ /. b₃,b₂, L~ b₁,b₁ /. 1,b₁ /. (len b₁)

proof end;

theorem Th26: :: JORDAN5C:26

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2)
for b₃ being Nat st b₁ is_S-Seq & 1 <= b₃ & b₃ + 1 <= len b₁ & b₂ in LSeg b₁,b₃ holds
LE b₂,b₁ /. (b₃ + 1), L~ b₁,b₁ /. 1,b₁ /. (len b₁)

proof end;

theorem Th27: :: JORDAN5C:27

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2)
for b₄, b₅ being Nat st L~ b₁ meets b₂ & b₁ is_S-Seq & b₂ is closed & First_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂ in LSeg b₁,b₄ & 1 <= b₄ & b₄ + 1 <= len b₁ & b₃ in LSeg b₁,b₅ & 1 <= b₅ & b₅ + 1 <= len b₁ & b₃ in b₂ & First_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂ <> b₃ holds
( b₄ <= b₅ & ( b₄ = b₅ implies LE First_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂,b₃,b₁ /. b₄,b₁ /. (b₄ + 1) ) )

proof end;

theorem Th28: :: JORDAN5C:28

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2)
for b₄, b₅ being Nat st L~ b₁ meets b₂ & b₁ is_S-Seq & b₂ is closed & Last_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂ in LSeg b₁,b₄ & 1 <= b₄ & b₄ + 1 <= len b₁ & b₃ in LSeg b₁,b₅ & 1 <= b₅ & b₅ + 1 <= len b₁ & b₃ in b₂ & Last_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂ <> b₃ holds
( b₄ >= b₅ & ( b₄ = b₅ implies LE b₃, Last_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂,b₁ /. b₄,b₁ /. (b₄ + 1) ) )

proof end;

theorem Th29: :: JORDAN5C:29

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being Point of (TOP-REAL 2)
for b₄ being Nat st b₂ in LSeg b₁,b₄ & b₃ in LSeg b₁,b₄ & b₁ is_S-Seq & 1 <= b₄ & b₄ + 1 <= len b₁ & LE b₂,b₃, L~ b₁,b₁ /. 1,b₁ /. (len b₁) holds
LE b₂,b₃, LSeg b₁,b₄,b₁ /. b₄,b₁ /. (b₄ + 1)

proof end;

theorem Th30: :: JORDAN5C:30

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being Point of (TOP-REAL 2) st b₂ in L~ b₁ & b₃ in L~ b₁ & b₁ is_S-Seq & b₂ <> b₃ holds
( LE b₂,b₃, L~ b₁,b₁ /. 1,b₁ /. (len b₁) iff for b₄, b₅ being Nat st b₂ in LSeg b₁,b₄ & b₃ in LSeg b₁,b₅ & 1 <= b₄ & b₄ + 1 <= len b₁ & 1 <= b₅ & b₅ + 1 <= len b₁ holds
( b₄ <= b₅ & ( b₄ = b₅ implies LE b₂,b₃,b₁ /. b₄,b₁ /. (b₄ + 1) ) ) )

proof end;