:: Subsequences of Standard Special Circular Sequences in $ { \cal E } ^2_ { \rm T } $
:: by Yatsuka Nakamura , Roman Matuszewski and Adam Grabowski
::
:: Received May 12, 1997
:: Copyright (c) 1997-2021 Association of Mizar Users

theorem Th1: :: JORDAN4:1

for i, j being Nat st j < i & i < j + j holds
i mod j <> 0

proof end;

theorem Th2: :: JORDAN4:2

for i, j being Nat st j <= i & i < j + j holds
( i mod j = i - j & i mod j = i -' j )

proof end;

theorem Th3: :: JORDAN4:3

for i, j being Nat holds (j + j) mod j = 0

proof end;

theorem Th4: :: JORDAN4:4

for j, k being Nat st 0 < k & k <= j & k mod j = 0 holds
k = j

proof end;

theorem Th5: :: JORDAN4:5

for D being non empty set
for f1 being FinSequence of D st f1 is circular & 1 <= len f1 holds
f1 . 1 = f1 . (len f1)

proof end;

theorem Th6: :: JORDAN4:6

for D being non empty set
for f1 being FinSequence of D
for k being Nat st k < len f1 holds
( (f1 /^ k) . (len (f1 /^ k)) = f1 . (len f1) & (f1 /^ k) /. (len (f1 /^ k)) = f1 /. (len f1) )

proof end;

theorem Th7: :: JORDAN4:7

for g being FinSequence of (TOP-REAL 2)
for i being Nat st g is being_S-Seq & i + 1 < len g holds
g /^ i is being_S-Seq

proof end;

theorem Th8: :: JORDAN4:8

for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Nat st 1 <= i2 & i2 <= i1 & i1 <= len f1 holds
len (mid (f1,i2,i1)) = (i1 -' i2) + 1

proof end;

theorem Th9: :: JORDAN4:9

for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Nat st 1 <= i2 & i2 <= i1 & i1 <= len f1 holds
len (mid (f1,i1,i2)) = (i1 -' i2) + 1

proof end;

theorem Th10: :: JORDAN4:10

for D being non empty set
for f1 being FinSequence of D
for i1, i2, j being Nat st 1 <= i1 & i1 <= i2 & i2 <= len f1 holds
(mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) = f1 . i2

proof end;

theorem Th11: :: JORDAN4:11

for D being non empty set
for f1 being FinSequence of D
for i1, i2, j being Nat st 1 <= i1 & i1 <= len f1 & 1 <= i2 & i2 <= len f1 holds
(mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) = f1 . i2

proof end;

theorem Th12: :: JORDAN4:12

for D being non empty set
for f1 being FinSequence of D
for i1, i2, j being Nat st 1 <= i2 & i2 <= i1 & i1 <= len f1 & 1 <= j & j <= (i1 -' i2) + 1 holds
(mid (f1,i1,i2)) . j = f1 . ((i1 -' j) + 1)

proof end;

theorem Th13: :: JORDAN4:13

for j being Nat
for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Nat st 1 <= i2 & i2 <= i1 & i1 <= len f1 & 1 <= j & j <= (i1 -' i2) + 1 holds
( (mid (f1,i1,i2)) . j = (mid (f1,i2,i1)) . ((((i1 - i2) + 1) - j) + 1) & (((i1 - i2) + 1) - j) + 1 = (((i1 -' i2) + 1) -' j) + 1 )

proof end;

theorem :: JORDAN4:14

for j being Nat
for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 <= len f1 & 1 <= j & j <= (i2 -' i1) + 1 holds
( (mid (f1,i1,i2)) . j = (mid (f1,i2,i1)) . ((((i2 - i1) + 1) - j) + 1) & (((i2 - i1) + 1) - j) + 1 = (((i2 -' i1) + 1) -' j) + 1 )

proof end;

theorem Th15: :: JORDAN4:15

for k being Nat
for f1 being FinSequence st k in dom f1 holds
( mid (f1,k,k) = <*(f1 . k)*> & len (mid (f1,k,k)) = 1 )

proof end;

theorem Th16: :: JORDAN4:16

for f1 being FinSequence holds mid (f1,0,0) = f1 | 1

proof end;

registration

cluster Relation-like empty Function-like FinSequence-like for set ;

existence
ex b₁ being FinSequence st b₁ is empty

proof end;

end;

registration

let f be empty FinSequence;
let k be Nat;

cluster f | k -> empty ;

coherence
f | k is empty by RELAT_1:82;

end;

theorem Th17: :: JORDAN4:17

for k being Nat
for f1 being FinSequence st len f1 < k holds
mid (f1,k,k) = {}

proof end;

theorem Th18: :: JORDAN4:18

for i1, i2 being Nat
for f1 being FinSequence holds mid (f1,i1,i2) = Rev (mid (f1,i2,i1))

proof end;

theorem Th19: :: JORDAN4:19

for f being FinSequence of (TOP-REAL 2)
for i1, i2, i being Nat st 1 <= i1 & i1 < i2 & i2 <= len f & 1 <= i & i < (i2 -' i1) + 1 holds
LSeg ((mid (f,i1,i2)),i) = LSeg (f,((i + i1) -' 1))

proof end;

theorem Th20: :: JORDAN4:20

for f being FinSequence of (TOP-REAL 2)
for i1, i2, i being Nat st 1 <= i1 & i1 < i2 & i2 <= len f & 1 <= i & i < (i2 -' i1) + 1 holds
LSeg ((mid (f,i2,i1)),i) = LSeg (f,(i2 -' i))

proof end;

definition

let n be Nat;
let f be FinSequence;

func S_Drop (n,f) -> Nat equals :Def1: :: JORDAN4:def 1
n mod ((len f) -' 1) if n mod ((len f) -' 1) <> 0
otherwise (len f) -' 1;

correctness
coherence
( ( n mod ((len f) -' 1) <> 0 implies n mod ((len f) -' 1) is Nat ) & ( not n mod ((len f) -' 1) <> 0 implies (len f) -' 1 is Nat ) );
consistency
for b₁ being Nat holds verum;
;

end;

:: deftheorem Def1 defines S_Drop JORDAN4:def 1 :
for n being Nat
for f being FinSequence holds
( ( n mod ((len f) -' 1) <> 0 implies S_Drop (n,f) = n mod ((len f) -' 1) ) & ( not n mod ((len f) -' 1) <> 0 implies S_Drop (n,f) = (len f) -' 1 ) );

theorem Th21: :: JORDAN4:21

for f being FinSequence holds S_Drop (((len f) -' 1),f) = (len f) -' 1

proof end;

theorem Th22: :: JORDAN4:22

for n being Nat
for f being FinSequence st 1 <= n & n <= (len f) -' 1 holds
S_Drop (n,f) = n

proof end;

theorem Th23: :: JORDAN4:23

for n being Nat
for f being FinSequence holds
( S_Drop (n,f) = S_Drop ((n + ((len f) -' 1)),f) & S_Drop (n,f) = S_Drop ((((len f) -' 1) + n),f) )

proof end;

definition

let f be V26() standard special_circular_sequence;
let g be FinSequence of (TOP-REAL 2);
let i1, i2 be Nat;

pred g is_a_part>_of f,i1,i2 means :: JORDAN4:def 2
( 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & g . (len g) = f . i2 & 1 <= len g & len g < len f & ( for i being Nat st 1 <= i & i <= len g holds
g . i = f . (S_Drop (((i1 + i) -' 1),f)) ) );

end;

:: deftheorem defines is_a_part>_of JORDAN4:def 2 :
for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat holds
( g is_a_part>_of f,i1,i2 iff ( 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & g . (len g) = f . i2 & 1 <= len g & len g < len f & ( for i being Nat st 1 <= i & i <= len g holds
g . i = f . (S_Drop (((i1 + i) -' 1),f)) ) ) );

definition

let f be V26() standard special_circular_sequence;
let g be FinSequence of (TOP-REAL 2);
let i1, i2 be Nat;

pred g is_a_part<_of f,i1,i2 means :: JORDAN4:def 3
( 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & g . (len g) = f . i2 & 1 <= len g & len g < len f & ( for i being Nat st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((((len f) + i1) -' i),f)) ) );

end;

:: deftheorem defines is_a_part<_of JORDAN4:def 3 :
for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat holds
( g is_a_part<_of f,i1,i2 iff ( 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & g . (len g) = f . i2 & 1 <= len g & len g < len f & ( for i being Nat st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((((len f) + i1) -' i),f)) ) ) );

definition

let f be V26() standard special_circular_sequence;
let g be FinSequence of (TOP-REAL 2);
let i1, i2 be Nat;

pred g is_a_part_of f,i1,i2 means :: JORDAN4:def 4
( g is_a_part>_of f,i1,i2 or g is_a_part<_of f,i1,i2 );

end;

:: deftheorem defines is_a_part_of JORDAN4:def 4 :
for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat holds
( g is_a_part_of f,i1,i2 iff ( g is_a_part>_of f,i1,i2 or g is_a_part<_of f,i1,i2 ) );

theorem :: JORDAN4:24

for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part_of f,i1,i2 holds
( 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & g . (len g) = f . i2 & 1 <= len g & len g < len f & ( for i being Nat st 1 <= i & i <= len g holds
g . i = f . (S_Drop (((i1 + i) -' 1),f)) or for i being Nat st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((((len f) + i1) -' i),f)) ) )

proof end;

theorem Th25: :: JORDAN4:25

for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part>_of f,i1,i2 & i1 <= i2 holds
( len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) )

proof end;

theorem Th26: :: JORDAN4:26

for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part>_of f,i1,i2 & i1 > i2 holds
( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) & g = (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) )

proof end;

theorem Th27: :: JORDAN4:27

for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part<_of f,i1,i2 & i1 >= i2 holds
( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) )

proof end;

theorem Th28: :: JORDAN4:28

for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part<_of f,i1,i2 & i1 < i2 holds
( len g = ((len f) + i1) -' i2 & g = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) )

proof end;

theorem Th29: :: JORDAN4:29

for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part>_of f,i1,i2 holds
Rev g is_a_part<_of f,i2,i1

proof end;

theorem Th30: :: JORDAN4:30

for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part<_of f,i1,i2 holds
Rev g is_a_part>_of f,i2,i1

proof end;

theorem Th31: :: JORDAN4:31

for f being V26() standard special_circular_sequence
for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 < len f holds
mid (f,i1,i2) is_a_part>_of f,i1,i2

proof end;

theorem Th32: :: JORDAN4:32

for f being V26() standard special_circular_sequence
for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 < len f holds
mid (f,i2,i1) is_a_part<_of f,i2,i1

proof end;

theorem Th33: :: JORDAN4:33

for f being V26() standard special_circular_sequence
for i1, i2 being Nat st 1 <= i2 & i1 > i2 & i1 < len f holds
(mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part>_of f,i1,i2

proof end;

theorem Th34: :: JORDAN4:34

for f being V26() standard special_circular_sequence
for i1, i2 being Nat st 1 <= i1 & i1 < i2 & i2 < len f holds
(mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part<_of f,i1,i2

proof end;

theorem Th35: :: JORDAN4:35

for h being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st 1 <= i1 & i1 <= len h & 1 <= i2 & i2 <= len h holds
L~ (mid (h,i1,i2)) c= L~ h

proof end;

theorem Th36: :: JORDAN4:36

for D being non empty set
for g being FinSequence of D holds
( g is one-to-one iff for i1, i2 being Nat st 1 <= i1 & i1 <= len g & 1 <= i2 & i2 <= len g & ( g . i1 = g . i2 or g /. i1 = g /. i2 ) holds
i1 = i2 )

proof end;

theorem Th37: :: JORDAN4:37

for f being V26() standard special_circular_sequence
for i2 being Nat st 1 < i2 & i2 + 1 <= len f holds
f | i2 is being_S-Seq

proof end;

theorem Th38: :: JORDAN4:38

for f being V26() standard special_circular_sequence
for i2 being Nat st 1 <= i2 & i2 + 1 < len f holds
f /^ i2 is being_S-Seq

proof end;

theorem Th39: :: JORDAN4:39

for f being V26() standard special_circular_sequence
for i1, i2 being Nat st 1 <= i1 & i1 < i2 & i2 + 1 <= len f holds
mid (f,i1,i2) is being_S-Seq

proof end;

theorem Th40: :: JORDAN4:40

for f being V26() standard special_circular_sequence
for i1, i2 being Nat st 1 < i1 & i1 < i2 & i2 <= len f holds
mid (f,i1,i2) is being_S-Seq

proof end;

theorem Th41: :: JORDAN4:41

for p0, p, q1, q2 being Point of (TOP-REAL 2) st p0 in LSeg (p,q1) & p0 in LSeg (p,q2) & p <> p0 & not q1 in LSeg (p,q2) holds
q2 in LSeg (p,q1)

proof end;

theorem Th42: :: JORDAN4:42

for f being V26() standard special_circular_sequence holds (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)}

proof end;

theorem Th43: :: JORDAN4:43

for f being V26() standard special_circular_sequence
for i1, i2 being Nat
for g1, g2 being FinSequence of (TOP-REAL 2) st 1 <= i1 & i1 < i2 & i2 < len f & g1 = mid (f,i1,i2) & g2 = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) holds
( (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f )

proof end;

theorem Th44: :: JORDAN4:44

for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part>_of f,i1,i2 & i1 < i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2

proof end;

Lm1: for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part>_of f,i1,i2 & i1 > i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2

proof end;

theorem :: JORDAN4:45

for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part<_of f,i1,i2 & i1 > i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2

proof end;

theorem Th46: :: JORDAN4:46

for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part>_of f,i1,i2 & i1 <> i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2

proof end;

theorem Th47: :: JORDAN4:47

for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part<_of f,i1,i2 & i1 <> i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2

proof end;

theorem Th48: :: JORDAN4:48

for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part_of f,i1,i2 & i1 <> i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2

proof end;

theorem :: JORDAN4:49

for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part_of f,i1,i2 & g . 1 <> g . (len g) holds
L~ g is_S-P_arc_joining f /. i1,f /. i2

proof end;

theorem Th50: :: JORDAN4:50

for f being V26() standard special_circular_sequence
for i1, i2 being Nat st 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & i1 <> i2 holds
ex g1, g2 being FinSequence of (TOP-REAL 2) st
( g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f & L~ g1 is_S-P_arc_joining f /. i1,f /. i2 & L~ g2 is_S-P_arc_joining f /. i1,f /. i2 & ( for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = g1 or g = g2 ) ) )

proof end;

theorem :: JORDAN4:51

for f being V26() standard special_circular_sequence
for P being non empty Subset of (TOP-REAL 2) st P = L~ f holds
P is being_simple_closed_curve

proof end;

theorem Th52: :: JORDAN4:52

for i1, i2 being Nat
for f being V26() standard special_circular_sequence
for g1, g2 being FinSequence of (TOP-REAL 2) st g1 is_a_part>_of f,i1,i2 & g2 is_a_part>_of f,i1,i2 holds
g1 = g2

proof end;

theorem Th53: :: JORDAN4:53

for i1, i2 being Nat
for f being V26() standard special_circular_sequence
for g1, g2 being FinSequence of (TOP-REAL 2) st g1 is_a_part<_of f,i1,i2 & g2 is_a_part<_of f,i1,i2 holds
g1 = g2

proof end;

theorem Th54: :: JORDAN4:54

for i1, i2 being Nat
for f being V26() standard special_circular_sequence
for g1, g2 being FinSequence of (TOP-REAL 2) st i1 <> i2 & g1 is_a_part>_of f,i1,i2 & g2 is_a_part<_of f,i1,i2 holds
g1 . 2 <> g2 . 2

proof end;

theorem Th55: :: JORDAN4:55

for i1, i2 being Nat
for f being V26() standard special_circular_sequence
for g1, g2 being FinSequence of (TOP-REAL 2) st i1 <> i2 & g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & g1 . 2 = g2 . 2 holds
g1 = g2

proof end;

definition

let f be V26() standard special_circular_sequence;
let i1, i2 be Element of NAT ;
assume that
A1: 1 <= i1 and
A2: i1 + 1 <= len f and
A3: 1 <= i2 and
A4: i2 + 1 <= len f and
A5: i1 <> i2 ;

func Lower (f,i1,i2) -> FinSequence of (TOP-REAL 2) means :: JORDAN4:def 5
( it is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies it . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 & (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies it . 2 = f . (S_Drop ((i1 -' 1),f)) ) );

correctness
existence
ex b₁ being FinSequence of (TOP-REAL 2) st
( b₁ is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies b₁ . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 & (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies b₁ . 2 = f . (S_Drop ((i1 -' 1),f)) ) );
uniqueness
for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₁ is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies b₁ . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 & (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies b₁ . 2 = f . (S_Drop ((i1 -' 1),f)) ) & b₂ is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies b₂ . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 & (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies b₂ . 2 = f . (S_Drop ((i1 -' 1),f)) ) holds
b₁ = b₂;

proof end;

func Upper (f,i1,i2) -> FinSequence of (TOP-REAL 2) means :: JORDAN4:def 6
( it is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies it . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies it . 2 = f . (S_Drop ((i1 -' 1),f)) ) );

correctness
existence
ex b₁ being FinSequence of (TOP-REAL 2) st
( b₁ is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies b₁ . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies b₁ . 2 = f . (S_Drop ((i1 -' 1),f)) ) );
uniqueness
for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₁ is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies b₁ . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies b₁ . 2 = f . (S_Drop ((i1 -' 1),f)) ) & b₂ is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies b₂ . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies b₂ . 2 = f . (S_Drop ((i1 -' 1),f)) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem defines Lower JORDAN4:def 5 :
for f being V26() standard special_circular_sequence
for i1, i2 being Element of NAT st 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & i1 <> i2 holds
for b₄ being FinSequence of (TOP-REAL 2) holds
( b₄ = Lower (f,i1,i2) iff ( b₄ is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies b₄ . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 & (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies b₄ . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) );

:: deftheorem defines Upper JORDAN4:def 6 :
for f being V26() standard special_circular_sequence
for i1, i2 being Element of NAT st 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & i1 <> i2 holds
for b₄ being FinSequence of (TOP-REAL 2) holds
( b₄ = Upper (f,i1,i2) iff ( b₄ is_a_part_of f,i1,i2 & ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies b₄ . 2 = f . (i1 + 1) ) & ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 & (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies b₄ . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) );