:: JORDAN5B semantic presentation

theorem Th1: :: JORDAN5B:1

for b₁ being Nat st 1 <= b₁ holds
b₁ -' 1 < b₁

proof end;

theorem Th2: :: JORDAN5B:2

for b₁, b₂ being Nat st b₁ + 1 <= b₂ holds
1 <= b₂ -' b₁

proof end;

theorem Th3: :: JORDAN5B:3

for b₁, b₂ being Nat st 1 <= b₁ & 1 <= b₂ holds
(b₂ -' b₁) + 1 <= b₂

proof end;

Lemma2: for b₁ being real number st 0 <= b₁ & b₁ <= 1 holds
( 0 <= 1 - b₁ & 1 - b₁ <= 1 )

proof end;

theorem Th4: :: JORDAN5B:4

for b₁ being real number st b₁ in the carrier of I[01] holds
1 - b₁ in the carrier of I[01]

proof end;

theorem Th5: :: JORDAN5B:5

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

proof end;

theorem Th6: :: JORDAN5B:6

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₁ `1 <> b₂ `1 & b₃ in LSeg b₁,b₂ & b₃ `1 = b₁ `1 holds
b₃ = b₁

proof end;

Lemma3: for b₁ being Point of I[01] holds b₁ is Real

proof end;

theorem Th7: :: JORDAN5B:7

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being Function of I[01] ,((TOP-REAL 2) | b₂)
for b₄ being Nat st 1 <= b₄ & b₄ + 1 <= len b₁ & b₁ is_S-Seq & b₂ = L~ b₁ & b₃ is_homeomorphism & b₃ . 0 = b₁ /. 1 & b₃ . 1 = b₁ /. (len b₁) holds
ex b₅, b₆ being Real st
( b₅ < b₆ & 0 <= b₅ & b₅ <= 1 & 0 <= b₆ & b₆ <= 1 & LSeg b₁,b₄ = b₃ .: [.b₅,b₆.] & b₃ . b₅ = b₁ /. b₄ & b₃ . b₆ = b₁ /. (b₄ + 1) )

proof end;

theorem Th8: :: JORDAN5B:8

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being non empty Subset of (TOP-REAL 2)
for b₄ being Function of I[01] ,((TOP-REAL 2) | b₂)
for b₅ being Nat
for b₆ being non empty Subset of I[01] st b₁ is_S-Seq & b₄ is_homeomorphism & b₄ . 0 = b₁ /. 1 & b₄ . 1 = b₁ /. (len b₁) & 1 <= b₅ & b₅ + 1 <= len b₁ & b₄ .: b₆ = LSeg b₁,b₅ & b₂ = L~ b₁ & b₃ = LSeg b₁,b₅ holds
ex b₇ being Function of (I[01] | b₆),((TOP-REAL 2) | b₃) st
( b₇ = b₄ | b₆ & b₇ is_homeomorphism )

proof end;

theorem Th9: :: JORDAN5B:9

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

proof end;

theorem Th10: :: JORDAN5B:10

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

proof end;

theorem Th11: :: JORDAN5B:11

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

proof end;

theorem Th12: :: JORDAN5B:12

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

proof end;

theorem Th13: :: JORDAN5B:13

for b₁, b₂ being Point of (TOP-REAL 2) st b₁ <> b₂ holds
LSeg b₁,b₂ = { b₃ where B is Point of (TOP-REAL 2) : ( LE b₁,b₃,b₁,b₂ & LE b₃,b₂,b₁,b₂ ) }

proof end;

theorem Th14: :: JORDAN5B:14

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

proof end;

theorem Th15: :: JORDAN5B:15

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

proof end;

theorem Th16: :: JORDAN5B:16

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

proof end;

theorem Th17: :: JORDAN5B:17

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₁ is_S-Seq & b₂ = b₁ . (len b₁) holds
L_Cut b₁,b₂ = <*b₂*>

proof end;

theorem Th18: :: JORDAN5B:18

canceled;

theorem Th19: :: JORDAN5B:19

canceled;

theorem Th20: :: JORDAN5B:20

canceled;

theorem Th21: :: JORDAN5B:21

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in L~ b₁ & b₂ <> b₁ . (len b₁) & b₁ is_S-Seq holds
Index b₂,(L_Cut b₁,b₂) = 1

proof end;

theorem Th22: :: JORDAN5B:22

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in L~ b₁ & b₁ is_S-Seq & b₂ <> b₁ . (len b₁) holds
b₂ in L~ (L_Cut b₁,b₂)

proof end;

theorem Th23: :: JORDAN5B:23

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in L~ b₁ & b₁ is_S-Seq & b₂ <> b₁ . 1 holds
b₂ in L~ (R_Cut b₁,b₂)

proof end;

theorem Th24: :: JORDAN5B:24

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in L~ b₁ & b₁ is one-to-one holds
B_Cut b₁,b₂,b₂ = <*b₂*>

proof end;

Lemma10: 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₂ <> b₁ . (len b₁) & b₃ <> b₁ . (len b₁) & b₁ is_S-Seq & not b₂ in L~ (L_Cut b₁,b₃) holds
b₃ in L~ (L_Cut b₁,b₂)

proof end;

theorem Th25: :: JORDAN5B:25

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₃ <> b₁ . (len b₁) & b₂ = b₁ . (len b₁) & b₁ is_S-Seq holds
b₂ in L~ (L_Cut b₁,b₃)

proof end;

theorem Th26: :: JORDAN5B:26

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being Point of (TOP-REAL 2) st ( b₂ <> b₁ . (len b₁) or b₃ <> b₁ . (len b₁) ) & b₂ in L~ b₁ & b₃ in L~ b₁ & b₁ is_S-Seq & not b₂ in L~ (L_Cut b₁,b₃) holds
b₃ in L~ (L_Cut b₁,b₂)

proof end;

Lemma12: 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₁ & ( Index b₂,b₁ < Index b₃,b₁ or ( Index b₂,b₁ = Index b₃,b₁ & LE b₂,b₃,b₁ /. (Index b₂,b₁),b₁ /. ((Index b₂,b₁) + 1) ) ) & b₂ <> b₃ holds
L~ (B_Cut b₁,b₂,b₃) c= L~ b₁

proof end;

theorem Th27: :: JORDAN5B:27

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 holds
L~ (B_Cut b₁,b₂,b₃) c= L~ b₁

proof end;

theorem Th28: :: JORDAN5B:28

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being Nat st 1 <= b₂ & b₃ <= len (GoB b₁) & b₂ < b₃ holds
(LSeg ((GoB b₁) * 1,(width (GoB b₁))),((GoB b₁) * b₂,(width (GoB b₁)))) /\ (LSeg ((GoB b₁) * b₃,(width (GoB b₁))),((GoB b₁) * (len (GoB b₁)),(width (GoB b₁)))) = {}

proof end;

theorem Th29: :: JORDAN5B:29

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being Nat st 1 <= b₂ & b₃ <= width (GoB b₁) & b₂ < b₃ holds
(LSeg ((GoB b₁) * (len (GoB b₁)),1),((GoB b₁) * (len (GoB b₁)),b₂)) /\ (LSeg ((GoB b₁) * (len (GoB b₁)),b₃),((GoB b₁) * (len (GoB b₁)),(width (GoB b₁)))) = {}

proof end;

theorem Th30: :: JORDAN5B:30

for b₁ being FinSequence of (TOP-REAL 2) st b₁ is_S-Seq holds
L_Cut b₁,(b₁ /. 1) = b₁

proof end;

theorem Th31: :: JORDAN5B:31

for b₁ being FinSequence of (TOP-REAL 2) st b₁ is_S-Seq holds
R_Cut b₁,(b₁ /. (len b₁)) = b₁

proof end;

theorem Th32: :: JORDAN5B:32

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in L~ b₁ holds
b₂ in LSeg (b₁ /. (Index b₂,b₁)),(b₁ /. ((Index b₂,b₁) + 1))

proof end;

theorem Th33: :: JORDAN5B:33

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st b₁ is unfolded & b₁ is s.n.c. & b₁ is one-to-one & len b₁ >= 2 & b₁ /. 1 in LSeg b₁,b₂ holds
b₂ = 1

proof end;

theorem Th34: :: JORDAN5B:34

for b₁ being non constant standard special_circular_sequence
for b₂ being Nat
for b₃ being Subset of (TOP-REAL 2) st 1 <= b₂ & b₂ <= width (GoB b₁) & b₃ = LSeg ((GoB b₁) * 1,b₂),((GoB b₁) * (len (GoB b₁)),b₂) holds
b₃ is_S-P_arc_joining (GoB b₁) * 1,b₂,(GoB b₁) * (len (GoB b₁)),b₂

proof end;

theorem Th35: :: JORDAN5B:35

for b₁ being non constant standard special_circular_sequence
for b₂ being Nat
for b₃ being Subset of (TOP-REAL 2) st 1 <= b₂ & b₂ <= len (GoB b₁) & b₃ = LSeg ((GoB b₁) * b₂,1),((GoB b₁) * b₂,(width (GoB b₁))) holds
b₃ is_S-P_arc_joining (GoB b₁) * b₂,1,(GoB b₁) * b₂,(width (GoB b₁))

proof end;

theorem Th36: :: JORDAN5B:36

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₁ & ( Index b₂,b₁ < Index b₃,b₁ or ( Index b₂,b₁ = Index b₃,b₁ & LE b₂,b₃,b₁ /. (Index b₂,b₁),b₁ /. ((Index b₂,b₁) + 1) ) ) & b₂ <> b₃ holds
L~ (B_Cut b₁,b₂,b₃) c= L~ b₁ by Lemma12;