:: 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-2012 Association of Mizar Users


begin

theorem Th1: :: JORDAN4:1
for i, j being Nat st j < i &amp; i < j + j holds
i mod j <> 0
proofend;

theorem Th2: :: JORDAN4:2
for i, j being Nat st j <= i &amp; i < j + j holds
( i mod j = i - j &amp; i mod j = i -' j )
proofend;

theorem Th3: :: JORDAN4:3
for i, j being Nat holds (j + j) mod j = 0
proofend;

theorem Th4: :: JORDAN4:4
for j, k being Nat st 0 < k &amp; k <= j &amp; k mod j = 0 holds
k = j
proofend;

begin

theorem Th5: :: JORDAN4:5
for D being non empty set
for f1 being FinSequence of D st f1 is circular &amp; 1 <= len f1 holds
f1 . 1 = f1 . (len f1)
proofend;

theorem Th6: :: JORDAN4:6
for D being non empty set
for f1 being FinSequence of D
for k being Element of NAT st k < len f1 holds
( (f1 /^ k) . (len (f1 /^ k)) = f1 . (len f1) &amp; (f1 /^ k) /. (len (f1 /^ k)) = f1 /. (len f1) )
proofend;

theorem Th7: :: JORDAN4:7
for g being FinSequence of (TOP-REAL 2)
for i being Element of NAT st g is being_S-Seq &amp; i + 1 < len g holds
g /^ i is being_S-Seq
proofend;

theorem Th8: :: JORDAN4:8
for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Element of NAT st 1 <= i2 &amp; i2 <= i1 &amp; i1 <= len f1 holds
len (mid (f1,i2,i1)) = (i1 -' i2) + 1
proofend;

theorem Th9: :: JORDAN4:9
for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Element of NAT st 1 <= i2 &amp; i2 <= i1 &amp; i1 <= len f1 holds
len (mid (f1,i1,i2)) = (i1 -' i2) + 1
proofend;

theorem Th10: :: JORDAN4:10
for D being non empty set
for f1 being FinSequence of D
for i1, i2, j being Element of NAT st 1 <= i1 &amp; i1 <= i2 &amp; i2 <= len f1 holds
(mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) = f1 . i2
proofend;

theorem Th11: :: JORDAN4:11
for D being non empty set
for f1 being FinSequence of D
for i1, i2, j being Element of NAT st 1 <= i1 &amp; i1 <= len f1 &amp; 1 <= i2 &amp; i2 <= len f1 holds
(mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) = f1 . i2
proofend;

theorem Th12: :: JORDAN4:12
for D being non empty set
for f1 being FinSequence of D
for i1, i2, j being Element of NAT st 1 <= i2 &amp; i2 <= i1 &amp; i1 <= len f1 &amp; 1 <= j &amp; j <= (i1 -' i2) + 1 holds
(mid (f1,i1,i2)) . j = f1 . ((i1 -' j) + 1)
proofend;

theorem Th13: :: JORDAN4:13
for j being Element of NAT
for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Element of NAT st 1 <= i2 &amp; i2 <= i1 &amp; i1 <= len f1 &amp; 1 <= j &amp; j <= (i1 -' i2) + 1 holds
( (mid (f1,i1,i2)) . j = (mid (f1,i2,i1)) . ((((i1 - i2) + 1) - j) + 1) &amp; (((i1 - i2) + 1) - j) + 1 = (((i1 -' i2) + 1) -' j) + 1 )
proofend;

theorem :: JORDAN4:14
for j being Element of NAT
for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Element of NAT st 1 <= i1 &amp; i1 <= i2 &amp; i2 <= len f1 &amp; 1 <= j &amp; j <= (i2 -' i1) + 1 holds
( (mid (f1,i1,i2)) . j = (mid (f1,i2,i1)) . ((((i2 - i1) + 1) - j) + 1) &amp; (((i2 - i1) + 1) - j) + 1 = (((i2 -' i1) + 1) -' j) + 1 )
proofend;

theorem Th15: :: JORDAN4:15
for D being non empty set
for f1 being FinSequence of D
for k being Element of NAT st 1 <= k &amp; k <= len f1 holds
( mid (f1,k,k) = <*(f1 /. k)*> &amp; len (mid (f1,k,k)) = 1 )
proofend;

theorem Th16: :: JORDAN4:16
for D being non empty set
for f1 being FinSequence of D holds mid (f1,0,0) = f1 | 1
proofend;

theorem Th17: :: JORDAN4:17
for D being non empty set
for f1 being FinSequence of D
for k being Element of NAT st len f1 < k holds
mid (f1,k,k) = <*> D
proofend;

theorem Th18: :: JORDAN4:18
for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Element of NAT holds mid (f1,i1,i2) = Rev (mid (f1,i2,i1))
proofend;

theorem Th19: :: JORDAN4:19
for f being FinSequence of (TOP-REAL 2)
for i1, i2, i being Element of NAT st 1 <= i1 &amp; i1 < i2 &amp; i2 <= len f &amp; 1 <= i &amp; i < (i2 -' i1) + 1 holds
LSeg ((mid (f,i1,i2)),i) = LSeg (f,((i + i1) -' 1))
proofend;

theorem Th20: :: JORDAN4:20
for f being FinSequence of (TOP-REAL 2)
for i1, i2, i being Element of NAT st 1 <= i1 &amp; i1 < i2 &amp; i2 <= len f &amp; 1 <= i &amp; i < (i2 -' i1) + 1 holds
LSeg ((mid (f,i2,i1)),i) = LSeg (f,(i2 -' i))
proofend;

begin

definition
let n be Element of NAT ;
let f be FinSequence;
func S_Drop (n,f) ->  Element of 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 Element of NAT ) &amp; ( not n mod ((len f) -' 1) <> 0 implies (len f) -' 1 is Element of NAT ) );
consistency
for b1 being Element of NAT holds verum;
;
end;

:: deftheorem Def1 defines S_Drop JORDAN4:def_1_:_
 for n being Element of NAT
for f being FinSequence holds
( ( n mod ((len f) -' 1) <> 0 implies S_Drop (n,f) = n mod ((len f) -' 1) ) &amp; ( 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
proofend;

theorem Th22: :: JORDAN4:22
for n being Element of NAT
for f being FinSequence st 1 <= n &amp; n <= (len f) -' 1 holds
S_Drop (n,f) = n
proofend;

theorem Th23: :: JORDAN4:23
for n being Element of NAT
for f being FinSequence holds
( S_Drop (n,f) = S_Drop ((n + ((len f) -' 1)),f) &amp; S_Drop (n,f) = S_Drop ((((len f) -' 1) + n),f) )
proofend;

definition
let f be non constant standard special_circular_sequence;
let g be FinSequence of (TOP-REAL 2);
let i1, i2 be Element of NAT ;
predg is_a_part>_of f,i1,i2 means :Def2: :: JORDAN4:def 2
( 1 <= i1 &amp; i1 + 1 <= len f &amp; 1 <= i2 &amp; i2 + 1 <= len f &amp; g . (len g) = f . i2 &amp; 1 <= len g &amp; len g < len f &amp; ( for i being Nat st 1 <= i &amp; i <= len g holds
g . i = f . (S_Drop (((i1 + i) -' 1),f)) ) );
end;

:: deftheorem Def2 defines is_a_part>_of JORDAN4:def_2_:_
 for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT holds
( g is_a_part>_of f,i1,i2 iff ( 1 <= i1 &amp; i1 + 1 <= len f &amp; 1 <= i2 &amp; i2 + 1 <= len f &amp; g . (len g) = f . i2 &amp; 1 <= len g &amp; len g < len f &amp; ( for i being Nat st 1 <= i &amp; i <= len g holds
g . i = f . (S_Drop (((i1 + i) -' 1),f)) ) ) );

definition
let f be non constant standard special_circular_sequence;
let g be FinSequence of (TOP-REAL 2);
let i1, i2 be Element of NAT ;
predg is_a_part<_of f,i1,i2 means :Def3: :: JORDAN4:def 3
( 1 <= i1 &amp; i1 + 1 <= len f &amp; 1 <= i2 &amp; i2 + 1 <= len f &amp; g . (len g) = f . i2 &amp; 1 <= len g &amp; len g < len f &amp; ( for i being Nat st 1 <= i &amp; i <= len g holds
g . i = f . (S_Drop ((((len f) + i1) -' i),f)) ) );
end;

:: deftheorem Def3 defines is_a_part<_of JORDAN4:def_3_:_
 for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT holds
( g is_a_part<_of f,i1,i2 iff ( 1 <= i1 &amp; i1 + 1 <= len f &amp; 1 <= i2 &amp; i2 + 1 <= len f &amp; g . (len g) = f . i2 &amp; 1 <= len g &amp; len g < len f &amp; ( for i being Nat st 1 <= i &amp; i <= len g holds
g . i = f . (S_Drop ((((len f) + i1) -' i),f)) ) ) );

definition
let f be non constant standard special_circular_sequence;
let g be FinSequence of (TOP-REAL 2);
let i1, i2 be Element of NAT ;
predg is_a_part_of f,i1,i2 means :Def4: :: JORDAN4:def 4
( g is_a_part>_of f,i1,i2 or g is_a_part<_of f,i1,i2 );
end;

:: deftheorem Def4 defines is_a_part_of JORDAN4:def_4_:_
 for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of 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 non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part_of f,i1,i2 holds
( 1 <= i1 &amp; i1 + 1 <= len f &amp; 1 <= i2 &amp; i2 + 1 <= len f &amp; g . (len g) = f . i2 &amp; 1 <= len g &amp; len g < len f &amp; ( for i being Element of NAT st 1 <= i &amp; i <= len g holds
g . i = f . (S_Drop (((i1 + i) -' 1),f)) or for i being Element of NAT st 1 <= i &amp; i <= len g holds
g . i = f . (S_Drop ((((len f) + i1) -' i),f)) ) )
proofend;

theorem Th25: :: JORDAN4:25
for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part>_of f,i1,i2 &amp; i1 <= i2 holds
( len g = (i2 -' i1) + 1 &amp; g = mid (f,i1,i2) )
proofend;

theorem Th26: :: JORDAN4:26
for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part>_of f,i1,i2 &amp; i1 > i2 holds
( len g = ((len f) + i2) -' i1 &amp; g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) &amp; g = (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) )
proofend;

theorem Th27: :: JORDAN4:27
for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part<_of f,i1,i2 &amp; i1 >= i2 holds
( len g = (i1 -' i2) + 1 &amp; g = mid (f,i1,i2) )
proofend;

theorem Th28: :: JORDAN4:28
for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part<_of f,i1,i2 &amp; i1 < i2 holds
( len g = ((len f) + i1) -' i2 &amp; g = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) )
proofend;

theorem Th29: :: JORDAN4:29
for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part>_of f,i1,i2 holds
Rev g is_a_part<_of f,i2,i1
proofend;

theorem Th30: :: JORDAN4:30
for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part<_of f,i1,i2 holds
Rev g is_a_part>_of f,i2,i1
proofend;

theorem Th31: :: JORDAN4:31
for f being non constant standard special_circular_sequence
for i1, i2 being Element of NAT st 1 <= i1 &amp; i1 <= i2 &amp; i2 < len f holds
mid (f,i1,i2) is_a_part>_of f,i1,i2
proofend;

theorem Th32: :: JORDAN4:32
for f being non constant standard special_circular_sequence
for i1, i2 being Element of NAT st 1 <= i1 &amp; i1 <= i2 &amp; i2 < len f holds
mid (f,i2,i1) is_a_part<_of f,i2,i1
proofend;

theorem Th33: :: JORDAN4:33
for f being non constant standard special_circular_sequence
for i1, i2 being Element of NAT st 1 <= i2 &amp; i1 > i2 &amp; i1 < len f holds
(mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part>_of f,i1,i2
proofend;

theorem Th34: :: JORDAN4:34
for f being non constant standard special_circular_sequence
for i1, i2 being Element of NAT st 1 <= i1 &amp; i1 < i2 &amp; i2 < len f holds
(mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part<_of f,i1,i2
proofend;

theorem Th35: :: JORDAN4:35
for h being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st 1 <= i1 &amp; i1 <= len h &amp; 1 <= i2 &amp; i2 <= len h holds
L~ (mid (h,i1,i2)) c= L~ h
proofend;

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 Element of NAT st 1 <= i1 &amp; i1 <= len g &amp; 1 <= i2 &amp; i2 <= len g &amp; ( g . i1 = g . i2 or g /. i1 = g /. i2 ) holds
i1 = i2 )
proofend;

theorem Th37: :: JORDAN4:37
for f being non constant standard special_circular_sequence
for i2 being Element of NAT st 1 < i2 &amp; i2 + 1 <= len f holds
f | i2 is being_S-Seq
proofend;

theorem Th38: :: JORDAN4:38
for f being non constant standard special_circular_sequence
for i2 being Element of NAT st 1 <= i2 &amp; i2 + 1 < len f holds
f /^ i2 is being_S-Seq
proofend;

theorem Th39: :: JORDAN4:39
for f being non constant standard special_circular_sequence
for i1, i2 being Element of NAT st 1 <= i1 &amp; i1 < i2 &amp; i2 + 1 <= len f holds
mid (f,i1,i2) is being_S-Seq
proofend;

theorem Th40: :: JORDAN4:40
for f being non constant standard special_circular_sequence
for i1, i2 being Element of NAT st 1 < i1 &amp; i1 < i2 &amp; i2 <= len f holds
mid (f,i1,i2) is being_S-Seq
proofend;

theorem Th41: :: JORDAN4:41
for p0, p, q1, q2 being Point of (TOP-REAL 2) st p0 in LSeg (p,q1) &amp; p0 in LSeg (p,q2) &amp; p <> p0 &amp; not q1 in LSeg (p,q2) holds
q2 in LSeg (p,q1)
proofend;

theorem Th42: :: JORDAN4:42
for f being non constant standard special_circular_sequence holds (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)}
proofend;

theorem Th43: :: JORDAN4:43
for f being non constant standard special_circular_sequence
for i1, i2 being Element of NAT
for g1, g2 being FinSequence of (TOP-REAL 2) st 1 <= i1 &amp; i1 < i2 &amp; i2 < len f &amp; g1 = mid (f,i1,i2) &amp; g2 = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) holds
( (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} &amp; (L~ g1) \/ (L~ g2) = L~ f )
proofend;

theorem Th44: :: JORDAN4:44
for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part>_of f,i1,i2 &amp; i1 < i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2
proofend;

Lm1:  for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part>_of f,i1,i2 &amp; i1 > i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2
proofend;

theorem :: JORDAN4:45
for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part<_of f,i1,i2 &amp; i1 > i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2
proofend;

theorem Th46: :: JORDAN4:46
for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part>_of f,i1,i2 &amp; i1 <> i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2
proofend;

theorem Th47: :: JORDAN4:47
for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part<_of f,i1,i2 &amp; i1 <> i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2
proofend;

theorem Th48: :: JORDAN4:48
for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part_of f,i1,i2 &amp; i1 <> i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2
proofend;

theorem :: JORDAN4:49
for f being non constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part_of f,i1,i2 &amp; g . 1 <> g . (len g) holds
L~ g is_S-P_arc_joining f /. i1,f /. i2
proofend;

theorem Th50: :: JORDAN4:50
for f being non constant standard special_circular_sequence
for i1, i2 being Element of NAT st 1 <= i1 &amp; i1 + 1 <= len f &amp; 1 <= i2 &amp; i2 + 1 <= len f &amp; i1 <> i2 holds
ex g1, g2 being FinSequence of (TOP-REAL 2) st
( g1 is_a_part_of f,i1,i2 &amp; g2 is_a_part_of f,i1,i2 &amp; (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} &amp; (L~ g1) \/ (L~ g2) = L~ f &amp; L~ g1 is_S-P_arc_joining f /. i1,f /. i2 &amp; L~ g2 is_S-P_arc_joining f /. i1,f /. i2 &amp; ( for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = g1 or g = g2 ) ) )
proofend;

theorem :: JORDAN4:51
for f being non constant 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
proofend;

theorem Th52: :: JORDAN4:52
for i1, i2 being Element of NAT
for f being non constant standard special_circular_sequence
for g1, g2 being FinSequence of (TOP-REAL 2) st g1 is_a_part>_of f,i1,i2 &amp; g2 is_a_part>_of f,i1,i2 holds
g1 = g2
proofend;

theorem Th53: :: JORDAN4:53
for i1, i2 being Element of NAT
for f being non constant standard special_circular_sequence
for g1, g2 being FinSequence of (TOP-REAL 2) st g1 is_a_part<_of f,i1,i2 &amp; g2 is_a_part<_of f,i1,i2 holds
g1 = g2
proofend;

theorem Th54: :: JORDAN4:54
for i1, i2 being Element of NAT
for f being non constant standard special_circular_sequence
for g1, g2 being FinSequence of (TOP-REAL 2) st i1 <> i2 &amp; g1 is_a_part>_of f,i1,i2 &amp; g2 is_a_part<_of f,i1,i2 holds
g1 . 2 <> g2 . 2
proofend;

theorem Th55: :: JORDAN4:55
for i1, i2 being Element of NAT
for f being non constant standard special_circular_sequence
for g1, g2 being FinSequence of (TOP-REAL 2) st i1 <> i2 &amp; g1 is_a_part_of f,i1,i2 &amp; g2 is_a_part_of f,i1,i2 &amp; g1 . 2 = g2 . 2 holds
g1 = g2
proofend;

definition
let f be non constant 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 &amp; ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies it . 2 = f . (i1 + 1) ) &amp; ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 &amp; (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies it . 2 = f . (S_Drop ((i1 -' 1),f)) ) );
correctness
existence
ex b1 being FinSequence of (TOP-REAL 2) st
( b1 is_a_part_of f,i1,i2 &amp; ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies b1 . 2 = f . (i1 + 1) ) &amp; ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 &amp; (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies b1 . 2 = f . (S_Drop ((i1 -' 1),f)) ) );
uniqueness
for b1, b2 being FinSequence of (TOP-REAL 2) st b1 is_a_part_of f,i1,i2 &amp; ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies b1 . 2 = f . (i1 + 1) ) &amp; ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 &amp; (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies b1 . 2 = f . (S_Drop ((i1 -' 1),f)) ) &amp; b2 is_a_part_of f,i1,i2 &amp; ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies b2 . 2 = f . (i1 + 1) ) &amp; ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 &amp; (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies b2 . 2 = f . (S_Drop ((i1 -' 1),f)) ) holds
b1 = b2;
proofend;
func Upper (f,i1,i2) ->  FinSequence of (TOP-REAL 2) means :: JORDAN4:def 6
( it is_a_part_of f,i1,i2 &amp; ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies it . 2 = f . (i1 + 1) ) &amp; ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 &amp; (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies it . 2 = f . (S_Drop ((i1 -' 1),f)) ) );
correctness
existence
ex b1 being FinSequence of (TOP-REAL 2) st
( b1 is_a_part_of f,i1,i2 &amp; ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies b1 . 2 = f . (i1 + 1) ) &amp; ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 &amp; (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies b1 . 2 = f . (S_Drop ((i1 -' 1),f)) ) );
uniqueness
for b1, b2 being FinSequence of (TOP-REAL 2) st b1 is_a_part_of f,i1,i2 &amp; ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies b1 . 2 = f . (i1 + 1) ) &amp; ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 &amp; (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies b1 . 2 = f . (S_Drop ((i1 -' 1),f)) ) &amp; b2 is_a_part_of f,i1,i2 &amp; ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies b2 . 2 = f . (i1 + 1) ) &amp; ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 &amp; (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies b2 . 2 = f . (S_Drop ((i1 -' 1),f)) ) holds
b1 = b2;
proofend;
end;

:: deftheorem  defines Lower JORDAN4:def_5_:_
 for f being non constant standard special_circular_sequence
for i1, i2 being Element of NAT st 1 <= i1 &amp; i1 + 1 <= len f &amp; 1 <= i2 &amp; i2 + 1 <= len f &amp; i1 <> i2 holds
for b4 being FinSequence of (TOP-REAL 2) holds
( b4 = Lower (f,i1,i2) iff ( b4 is_a_part_of f,i1,i2 &amp; ( ( (f /. (i1 + 1)) `1 < (f /. i1) `1 or (f /. (i1 + 1)) `2 < (f /. i1) `2 ) implies b4 . 2 = f . (i1 + 1) ) &amp; ( (f /. (i1 + 1)) `1 >= (f /. i1) `1 &amp; (f /. (i1 + 1)) `2 >= (f /. i1) `2 implies b4 . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) );

:: deftheorem  defines Upper JORDAN4:def_6_:_
 for f being non constant standard special_circular_sequence
for i1, i2 being Element of NAT st 1 <= i1 &amp; i1 + 1 <= len f &amp; 1 <= i2 &amp; i2 + 1 <= len f &amp; i1 <> i2 holds
for b4 being FinSequence of (TOP-REAL 2) holds
( b4 = Upper (f,i1,i2) iff ( b4 is_a_part_of f,i1,i2 &amp; ( ( (f /. (i1 + 1)) `1 > (f /. i1) `1 or (f /. (i1 + 1)) `2 > (f /. i1) `2 ) implies b4 . 2 = f . (i1 + 1) ) &amp; ( (f /. (i1 + 1)) `1 <= (f /. i1) `1 &amp; (f /. (i1 + 1)) `2 <= (f /. i1) `2 implies b4 . 2 = f . (S_Drop ((i1 -' 1),f)) ) ) );