:: deftheorem defines Upper JORDAN4:def 6 :
for f being constant 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)) ) ) );