for b₁, b₂ being natural number st ( b₁ + 2 <= b₂ or (b₁ + 1) + 1 <= b₂ ) holds
( b₁ + 1 < b₂ & (b₁ + 1) -' 1 < b₂ & (b₁ + 1) -' 2 < b₂ & b₁ + 1 <= b₂ & (b₁ -' 1) + 1 < b₂ & ((b₁ -' 1) + 1) -' 1 < b₂ & b₁ < b₂ & b₁ -' 1 < b₂ & b₁ -' 2 < b₂ & b₁ <= b₂ )

proof end;

theorem Th11: :: JORDAN3:11

for b₁, b₂ being natural number st ( b₁ <= b₂ or b₁ <= b₂ -' 1 ) holds
( b₁ < b₂ + 1 & b₁ <= b₂ + 1 & b₁ < (b₂ + 1) + 1 & b₁ <= (b₂ + 1) + 1 & b₁ < b₂ + 2 & b₁ <= b₂ + 2 )

proof end;

theorem Th12: :: JORDAN3:12

for b₁, b₂ being natural number st ( b₁ < b₂ or b₁ + 1 <= b₂ ) holds
b₁ <= b₂ -' 1

proof end;

theorem Th13: :: JORDAN3:13

for b₁, b₂, b₃ being natural number st b₁ >= b₂ holds
b₁ >= b₂ -' b₃

proof end;

theorem Th14: :: JORDAN3:14

for b₁, b₂ being natural number st 1 <= b₁ & 1 <= b₂ -' b₁ holds
b₂ -' b₁ < b₂

proof end;

theorem Th15: :: JORDAN3:15

for b₁ being Nat
for b₂, b₃ being FinSequence st len b₂ < b₁ & ( b₁ <= (len b₂) + (len b₃) or b₁ <= len (b₂ ^ b₃) ) holds
(b₂ ^ b₃) . b₁ = b₃ . (b₁ - (len b₂))

proof end;

theorem Th16: :: JORDAN3:16

canceled;

theorem Th17: :: JORDAN3:17

for b₁ being non empty set
for b₂ being set
for b₃ being FinSequence of b₁ st 1 <= len b₃ holds
( (b₃ ^ <*b₂*>) . 1 = b₃ . 1 & (b₃ ^ <*b₂*>) . 1 = b₃ /. 1 & (<*b₂*> ^ b₃) . ((len b₃) + 1) = b₃ . (len b₃) & (<*b₂*> ^ b₃) . ((len b₃) + 1) = b₃ /. (len b₃) )

proof end;

theorem Th18: :: JORDAN3:18

for b₁ being FinSequence st len b₁ = 1 holds
Rev b₁ = b₁

proof end;

theorem Th19: :: JORDAN3:19

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Nat holds len (b₂ /^ b₃) = (len b₂) -' b₃

proof end;

theorem Th20: :: JORDAN3:20

canceled;

theorem Th21: :: JORDAN3:21

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat holds (b₂ /^ b₃) | (b₄ -' b₃) = (b₂ | b₄) /^ b₃

proof end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
let c₃, c₄ be Nat;
func mid c₂,c₃,c₄ -> FinSequence of a₁ equals :Def1: :: JORDAN3:def 1
(a₂ /^ (a₃ -' 1)) | ((a₄ -' a₃) + 1) if a₃ <= a₄
otherwise Rev ((a₂ /^ (a₄ -' 1)) | ((a₃ -' a₄) + 1));
correctness ;

end;

:: deftheorem Def1 defines mid JORDAN3:def 1 :

theorem Th22: :: JORDAN3:22

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat st 1 <= b₃ & b₃ <= len b₂ & 1 <= b₄ & b₄ <= len b₂ holds
Rev (mid b₂,b₃,b₄) = mid (Rev b₂),(((len b₂) -' b₄) + 1),(((len b₂) -' b₃) + 1)

proof end;

theorem Th23: :: JORDAN3:23

for b₁ being non empty set
for b₂, b₃ being Nat
for b₄ being FinSequence of b₁ st 1 <= b₃ & b₃ + b₂ <= len b₄ holds
(b₄ /^ b₂) . b₃ = b₄ . (b₃ + b₂)

proof end;

theorem Th24: :: JORDAN3:24

for b₁ being non empty set
for b₂ being Nat
for b₃ being FinSequence of b₁ st 1 <= b₂ & b₂ <= len b₃ holds
(Rev b₃) . b₂ = b₃ . (((len b₃) - b₂) + 1)

proof end;

theorem Th25: :: JORDAN3:25

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Nat st 1 <= b₃ holds
mid b₂,1,b₃ = b₂ | b₃

proof end;

theorem Th26: :: JORDAN3:26

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Nat st b₃ <= len b₂ holds
mid b₂,b₃,(len b₂) = b₂ /^ (b₃ -' 1)

proof end;

theorem Th27: :: JORDAN3:27

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat st 1 <= b₃ & b₃ <= len b₂ & 1 <= b₄ & b₄ <= len b₂ holds
( (mid b₂,b₃,b₄) . 1 = b₂ . b₃ & ( b₃ <= b₄ implies ( len (mid b₂,b₃,b₄) = (b₄ -' b₃) + 1 & ( for b₅ being Nat st 1 <= b₅ & b₅ <= len (mid b₂,b₃,b₄) holds
(mid b₂,b₃,b₄) . b₅ = b₂ . ((b₅ + b₃) -' 1) ) ) ) & ( b₃ > b₄ implies ( len (mid b₂,b₃,b₄) = (b₃ -' b₄) + 1 & ( for b₅ being Nat st 1 <= b₅ & b₅ <= len (mid b₂,b₃,b₄) holds
(mid b₂,b₃,b₄) . b₅ = b₂ . ((b₃ -' b₅) + 1) ) ) ) )

proof end;

theorem Th28: :: JORDAN3:28

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat holds rng (mid b₂,b₃,b₄) c= rng b₂

proof end;

theorem Th29: :: JORDAN3:29

for b₁ being non empty set
for b₂ being FinSequence of b₁ st 1 <= len b₂ holds
mid b₂,1,(len b₂) = b₂

proof end;

theorem Th30: :: JORDAN3:30

for b₁ being non empty set
for b₂ being FinSequence of b₁ st 1 <= len b₂ holds
mid b₂,(len b₂),1 = Rev b₂

proof end;

theorem Th31: :: JORDAN3:31

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄, b₅ being Nat st 1 <= b₃ & b₃ <= b₄ & b₄ <= len b₂ & 1 <= b₅ & ( b₅ <= (b₄ -' b₃) + 1 or b₅ <= (b₄ - b₃) + 1 or b₅ <= (b₄ + 1) - b₃ ) holds
( (mid b₂,b₃,b₄) . b₅ = b₂ . ((b₅ + b₃) -' 1) & (mid b₂,b₃,b₄) . b₅ = b₂ . ((b₅ -' 1) + b₃) & (mid b₂,b₃,b₄) . b₅ = b₂ . ((b₅ + b₃) - 1) & (mid b₂,b₃,b₄) . b₅ = b₂ . ((b₅ - 1) + b₃) )

proof end;

theorem Th32: :: JORDAN3:32

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat st 1 <= b₄ & b₄ <= b₃ & b₃ <= len b₂ holds
(mid b₂,1,b₃) . b₄ = b₂ . b₄

proof end;

theorem Th33: :: JORDAN3:33

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat st 1 <= b₃ & b₃ <= b₄ & b₄ <= len b₂ holds
len (mid b₂,b₃,b₄) <= len b₂

proof end;

theorem Th34: :: JORDAN3:34

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

proof end;

theorem Th35: :: JORDAN3:35

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

proof end;

theorem Th36: :: JORDAN3:36

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2) st ( b₁ `1 = b₂ `1 or b₁ `2 = b₂ `2 ) & LSeg b₃,b₄ c= LSeg b₁,b₂ & not b₃ `1 = b₄ `1 holds
b₃ `2 = b₄ `2

proof end;

theorem Th37: :: JORDAN3:37

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st 2 <= b₂ & b₁ is_S-Seq holds
b₁ | b₂ is_S-Seq

proof end;

theorem Th38: :: JORDAN3:38

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st b₂ <= len b₁ & 2 <= (len b₁) -' b₂ & b₁ is_S-Seq holds
b₁ /^ b₂ is_S-Seq

proof end;

theorem Th39: :: JORDAN3:39

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being Nat st b₁ is_S-Seq & 1 <= b₂ & b₂ <= len b₁ & 1 <= b₃ & b₃ <= len b₁ & b₂ <> b₃ holds
mid b₁,b₂,b₃ is_S-Seq

proof end;

definition

let c₁ be FinSequence of (TOP-REAL 2);
let c₂ be Point of (TOP-REAL 2);
assume E31: c₂ in L~ c₁ ;
func Index c₂,c₁ -> Nat means :Def2: :: JORDAN3:def 2
ex b₁ being non empty Subset of NAT st
( a₃ = min b₁ & b₁ = { b₂ where B is Nat : a₂ in LSeg a₁,b₂ } );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines Index JORDAN3:def 2 :

theorem Th40: :: JORDAN3:40

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2)
for b₃ being Nat st b₂ in LSeg b₁,b₃ holds
Index b₂,b₁ <= b₃

proof end;

theorem Th41: :: JORDAN3:41

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

proof end;

theorem Th42: :: JORDAN3:42

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₁)

proof end;

theorem Th43: :: JORDAN3:43

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in LSeg b₁,1 holds
Index b₂,b₁ = 1

proof end;

theorem Th44: :: JORDAN3:44

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st len b₁ >= 2 holds
Index (b₁ /. 1),b₁ = 1

proof end;

theorem Th45: :: JORDAN3:45

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₃ <= len b₁ & b₂ = b₁ . b₃ holds
(Index b₂,b₁) + 1 = b₃

proof end;

theorem Th46: :: JORDAN3:46

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2)
for b₃ being Nat st b₁ is s.n.c. & b₂ in LSeg b₁,b₃ & not b₃ = Index b₂,b₁ holds
b₃ = (Index b₂,b₁) + 1

proof end;

theorem Th47: :: JORDAN3:47

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2)
for b₃ being Nat st b₁ is unfolded & b₁ is s.n.c. & b₃ + 1 <= len b₁ & b₂ in LSeg b₁,b₃ & b₂ <> b₁ . b₃ holds
b₃ = Index b₂,b₁

proof end;

definition

let c₁ be FinSequence of (TOP-REAL 2);
let c₂, c₃ be Point of (TOP-REAL 2);
pred c₁ is_S-Seq_joining c₂,c₃ means :Def3: :: JORDAN3:def 3
( a₁ is_S-Seq & a₁ . 1 = a₂ & a₁ . (len a₁) = a₃ );

end;

:: deftheorem Def3 defines is_S-Seq_joining JORDAN3:def 3 :

theorem Th48: :: JORDAN3:48

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being Point of (TOP-REAL 2) st b₁ is_S-Seq_joining b₂,b₃ holds
Rev b₁ is_S-Seq_joining b₃,b₂

proof end;

theorem Th49: :: JORDAN3:49

for b₁, b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2)
for b₄ being Nat st b₃ in L~ b₁ & b₂ = <*b₃*> ^ (mid b₁,((Index b₃,b₁) + 1),(len b₁)) & 1 <= b₄ & b₄ + 1 <= len b₂ holds
LSeg b₂,b₄ c= LSeg b₁,(((Index b₃,b₁) + b₄) -' 1)

proof end;

theorem Th50: :: JORDAN3:50

for b₁, b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₁ is_S-Seq & b₃ in L~ b₁ & b₃ <> b₁ . ((Index b₃,b₁) + 1) & b₂ = <*b₃*> ^ (mid b₁,((Index b₃,b₁) + 1),(len b₁)) holds
b₂ is_S-Seq_joining b₃,b₁ /. (len b₁)

proof end;

theorem Th51: :: JORDAN3:51

for b₁, b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2)
for b₄ being Nat st b₃ in L~ b₁ & 1 <= b₄ & b₄ + 1 <= len b₂ & b₂ = (mid b₁,1,(Index b₃,b₁)) ^ <*b₃*> holds
LSeg b₂,b₄ c= LSeg b₁,b₄

proof end;

theorem Th52: :: JORDAN3:52

for b₁, b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₁ is_S-Seq & b₃ in L~ b₁ & b₃ <> b₁ . 1 & b₂ = (mid b₁,1,(Index b₃,b₁)) ^ <*b₃*> holds
b₂ is_S-Seq_joining b₁ /. 1,b₃

proof end;

definition

let c₁ be FinSequence of (TOP-REAL 2);
let c₂ be Point of (TOP-REAL 2);
func L_Cut c₁,c₂ -> FinSequence of (TOP-REAL 2) equals :Def4: :: JORDAN3:def 4
<*a₂*> ^ (mid a₁,((Index a₂,a₁) + 1),(len a₁)) if a₂ <> a₁ . ((Index a₂,a₁) + 1)
otherwise mid a₁,((Index a₂,a₁) + 1),(len a₁);
correctness ;
func R_Cut c₁,c₂ -> FinSequence of (TOP-REAL 2) equals :Def5: :: JORDAN3:def 5
(mid a₁,1,(Index a₂,a₁)) ^ <*a₂*> if a₂ <> a₁ . 1
otherwise <*a₂*>;
correctness ;

end;

:: deftheorem Def4 defines L_Cut JORDAN3:def 4 :

:: deftheorem Def5 defines R_Cut JORDAN3:def 5 :

theorem Th53: :: JORDAN3:53

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

proof end;

theorem Th54: :: JORDAN3:54

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₁ is unfolded & b₁ is s.n.c. & b₂ in L~ b₁ & b₂ <> b₁ . ((Index b₂,b₁) + 1) holds
(Index b₂,(Rev b₁)) + (Index b₂,b₁) = len b₁

proof end;

theorem Th55: :: JORDAN3:55

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Nat
for b₄ being Element of b₁ holds (<*b₄*> ^ b₂) | (b₃ + 1) = <*b₄*> ^ (b₂ | b₃)

proof end;

theorem Th56: :: JORDAN3:56

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat st b₃ < b₄ & b₃ in dom b₂ holds
mid b₂,b₃,b₄ = <*(b₂ . b₃)*> ^ (mid b₂,(b₃ + 1),b₄)

proof end;

registration

let c₁ be non empty FinSequence;
cluster Rev a₁ -> non empty ;
coherence

proof end;

end;

theorem Th57: :: JORDAN3:57

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₁ is_S-Seq & b₂ in L~ b₁ holds
L_Cut (Rev b₁),b₂ = Rev (R_Cut b₁,b₂)

proof end;

theorem Th58: :: JORDAN3:58

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

proof end;

theorem Th59: :: JORDAN3:59

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in L~ b₁ holds
( (R_Cut b₁,b₂) . (len (R_Cut b₁,b₂)) = b₂ & ( for b₃ being Nat st 1 <= b₃ & b₃ <= Index b₂,b₁ holds
(R_Cut b₁,b₂) . b₃ = b₁ . b₃ ) )

proof end;

theorem Th60: :: JORDAN3:60

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

proof end;

theorem Th61: :: JORDAN3:61

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

proof end;

definition

let c₁, c₂, c₃, c₄ be Point of (TOP-REAL 2);
pred LE c₃,c₄,c₁,c₂ means :Def6: :: JORDAN3:def 6
( a₃ in LSeg a₁,a₂ & a₄ in LSeg a₁,a₂ & ( for b₁, b₂ being Real st 0 <= b₁ & b₁ <= 1 & a₃ = ((1 - b₁) * a₁) + (b₁ * a₂) & 0 <= b₂ & b₂ <= 1 & a₄ = ((1 - b₂) * a₁) + (b₂ * a₂) holds
b₁ <= b₂ ) );

end;

:: deftheorem Def6 defines LE JORDAN3:def 6 :

definition

let c₁, c₂, c₃, c₄ be Point of (TOP-REAL 2);
pred LT c₃,c₄,c₁,c₂ means :Def7: :: JORDAN3:def 7
( LE a₃,a₄,a₁,a₂ & a₃ <> a₄ );

end;

:: deftheorem Def7 defines LT JORDAN3:def 7 :

theorem Th62: :: JORDAN3:62

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

proof end;

theorem Th63: :: JORDAN3:63

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

proof end;

theorem Th64: :: JORDAN3:64

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₁ holds
b₃ in L~ (L_Cut b₁,b₂)

proof end;

theorem Th65: :: JORDAN3:65

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

proof end;

theorem Th66: :: JORDAN3:66

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₃ & Index b₂,b₁ = Index b₃,b₁ & LE b₂,b₃,b₁ /. (Index b₂,b₁),b₁ /. ((Index b₂,b₁) + 1) holds
b₃ in L~ (L_Cut b₁,b₂)

proof end;

definition

let c₁ be FinSequence of (TOP-REAL 2);
let c₂, c₃ be Point of (TOP-REAL 2);
func B_Cut c₁,c₂,c₃ -> FinSequence of (TOP-REAL 2) equals :Def8: :: JORDAN3:def 8
R_Cut (L_Cut a₁,a₂),a₃ if ( ( a₂ in L~ a₁ & a₃ in L~ a₁ & Index a₂,a₁ < Index a₃,a₁ ) or ( Index a₂,a₁ = Index a₃,a₁ & LE a₂,a₃,a₁ /. (Index a₂,a₁),a₁ /. ((Index a₂,a₁) + 1) ) )
otherwise Rev (R_Cut (L_Cut a₁,a₃),a₂);
correctness ;

end;

:: deftheorem Def8 defines B_Cut JORDAN3:def 8 :

theorem Th67: :: JORDAN3:67

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

proof end;

theorem Th68: :: JORDAN3:68

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

proof end;

theorem Th69: :: JORDAN3:69

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

proof end;

theorem Th70: :: JORDAN3:70

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

proof end;

Lemma66: for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being Point of (TOP-REAL 2) st b₁ is_S-Seq & b₂ in L~ b₁ & b₃ in L~ b₁ & b₂ <> 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) ) ) holds
B_Cut b₁,b₂,b₃ is_S-Seq_joining b₂,b₃

proof end;

theorem Th71: :: JORDAN3:71

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

proof end;

theorem Th72: :: JORDAN3:72

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

proof end;

theorem Th73: :: JORDAN3:73

for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₁ . (len b₁) = b₂ . 1 & b₁ is_S-Seq & b₂ is_S-Seq & (L~ b₁) /\ (L~ b₂) = {(b₂ . 1)} holds
b₁ ^ (mid b₂,2,(len b₂)) is_S-Seq

proof end;

theorem Th74: :: JORDAN3:74

for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₁ . (len b₁) = b₂ . 1 & b₁ is_S-Seq & b₂ is_S-Seq & (L~ b₁) /\ (L~ b₂) = {(b₂ . 1)} holds
b₁ ^ (mid b₂,2,(len b₂)) is_S-Seq_joining b₁ /. 1,b₂ /. (len b₂)

proof end;

theorem Th75: :: JORDAN3:75

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat holds L~ (b₁ /^ b₂) c= L~ b₁

proof end;

theorem Th76: :: JORDAN3:76

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in L~ b₁ holds
L~ (R_Cut b₁,b₂) c= L~ b₁

proof end;

Lemma71: for b₁ being natural number
for b₂, b₃ being Nat st b₂ <= b₃ holds
(b₃ + b₁) -' b₂ = (b₃ + b₁) - b₂

proof end;

Lemma72: for b₁ being Nat
for b₂ being non empty set holds (<*> b₂) | b₁ = <*> b₂

proof end;

Lemma73: for b₁ being non empty set holds Rev (<*> b₁) = <*> b₁
;

Lemma74: for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Nat st 1 <= b₃ & b₃ <= len b₂ holds
( mid b₂,b₃,b₃ = <*(b₂ /. b₃)*> & len (mid b₂,b₃,b₃) = 1 )

proof end;

Lemma75: for b₁ being non empty set
for b₂ being FinSequence of b₁ holds mid b₂,0,0 = b₂ | 1

proof end;

Lemma76: for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Nat st len b₂ < b₃ holds
mid b₂,b₃,b₃ = <*> b₁

proof end;

Lemma77: for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat holds mid b₂,b₃,b₄ = Rev (mid b₂,b₄,b₃)

proof end;

Lemma78: for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being Nat st 1 <= b₂ & b₂ <= len b₁ & 1 <= b₃ & b₃ <= len b₁ holds
L~ (mid b₁,b₂,b₃) c= L~ b₁

proof end;

Lemma79: for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being FinSequence of b₃ st b₁ in dom b₄ & b₂ in dom b₄ holds
len (mid b₄,b₁,b₂) >= 1

proof end;

Lemma80: for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being FinSequence of b₃ st b₁ in dom b₄ & b₂ in dom b₄ holds
not mid b₄,b₁,b₂ is empty

proof end;

Lemma81: for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being FinSequence of b₃ st b₁ in dom b₄ & b₂ in dom b₄ holds
(mid b₄,b₁,b₂) /. 1 = b₄ /. b₁

proof end;

theorem Th77: :: JORDAN3:77

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in L~ b₁ holds
L~ (L_Cut b₁,b₂) c= L~ b₁

proof end;

theorem Th78: :: JORDAN3:78

for b₁, b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₁ . (len b₁) = b₂ . 1 & b₃ in L~ b₁ & b₁ is_S-Seq & b₂ is_S-Seq & (L~ b₁) /\ (L~ b₂) = {(b₂ . 1)} & b₃ <> b₁ . (len b₁) holds
(L_Cut b₁,b₃) ^ (mid b₂,2,(len b₂)) is_S-Seq_joining b₃,b₂ /. (len b₂)

proof end;

theorem Th79: :: JORDAN3:79

proof end;

theorem Th80: :: JORDAN3:80

for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₁ . (len b₁) = b₂ . 1 & b₁ is_S-Seq & b₂ is_S-Seq & (L~ b₁) /\ (L~ b₂) = {(b₂ . 1)} holds
(mid b₁,1,((len b₁) -' 1)) ^ b₂ is_S-Seq

proof end;

theorem Th81: :: JORDAN3:81

for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₁ . (len b₁) = b₂ . 1 & b₁ is_S-Seq & b₂ is_S-Seq & (L~ b₁) /\ (L~ b₂) = {(b₂ . 1)} holds
(mid b₁,1,((len b₁) -' 1)) ^ b₂ is_S-Seq_joining b₁ /. 1,b₂ /. (len b₂)

proof end;

theorem Th82: :: JORDAN3:82

for b₁, b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₁ . (len b₁) = b₂ . 1 & b₃ in L~ b₂ & b₁ is_S-Seq & b₂ is_S-Seq & (L~ b₁) /\ (L~ b₂) = {(b₂ . 1)} & b₃ <> b₂ . 1 holds
(mid b₁,1,((len b₁) -' 1)) ^ (R_Cut b₂,b₃) is_S-Seq_joining b₁ /. 1,b₃

proof end;

theorem Th83: :: JORDAN3:83

proof end;