:: JORDAN4 semantic presentation

theorem Th1: :: JORDAN4:1

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

proof end;

theorem Th2: :: JORDAN4:2

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

proof end;

theorem Th3: :: JORDAN4:3

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

proof end;

theorem Th4: :: JORDAN4:4

for b₁, b₂, b₃ being Nat st b₁ <> 0 & b₂ = b₃ * b₁ holds
b₃ <= b₂

proof end;

theorem Th5: :: JORDAN4:5

for b₁, b₂ being Nat st b₁ < b₂ holds
b₁ div b₂ = 0

proof end;

theorem Th6: :: JORDAN4:6

for b₁, b₂ being Nat st 0 < b₁ & b₁ < b₂ & b₂ < b₁ + b₁ holds
b₂ mod b₁ <> 0

proof end;

theorem Th7: :: JORDAN4:7

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

proof end;

theorem Th8: :: JORDAN4:8

for b₁ being Nat holds (b₁ + b₁) mod b₁ = 0

proof end;

theorem Th9: :: JORDAN4:9

for b₁, b₂ being Nat st 0 < b₁ & b₁ <= b₂ & b₁ mod b₂ = 0 holds
b₁ = b₂

proof end;

theorem Th10: :: JORDAN4:10

canceled;

theorem Th11: :: JORDAN4:11

canceled;

theorem Th12: :: JORDAN4:12

canceled;

theorem Th13: :: JORDAN4:13

canceled;

theorem Th14: :: JORDAN4:14

for b₁ being non empty set
for b₂ being FinSequence of b₁ st b₂ is circular & 1 <= len b₂ holds
b₂ . 1 = b₂ . (len b₂)

proof end;

theorem Th15: :: JORDAN4:15

canceled;

theorem Th16: :: JORDAN4:16

canceled;

theorem Th17: :: JORDAN4:17

canceled;

theorem Th18: :: JORDAN4:18

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

proof end;

theorem Th19: :: JORDAN4:19

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

proof end;

theorem Th20: :: JORDAN4:20

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₃) = (b₃ -' b₄) + 1

proof end;

theorem Th21: :: JORDAN4:21

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₄) = (b₃ -' b₄) + 1

proof end;

theorem Th22: :: JORDAN4:22

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₂ holds
(mid b₂,b₃,b₄) . (len (mid b₂,b₃,b₄)) = b₂ . b₄

proof end;

theorem Th23: :: JORDAN4:23

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

proof end;

theorem Th24: :: JORDAN4:24

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 holds
(mid b₂,b₃,b₄) . b₅ = b₂ . ((b₃ -' b₅) + 1)

proof end;

theorem Th25: :: JORDAN4:25

for b₁ being Nat
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₃ & 1 <= b₁ & b₁ <= (b₄ -' b₅) + 1 holds
( (mid b₃,b₄,b₅) . b₁ = (mid b₃,b₅,b₄) . ((((b₄ - b₅) + 1) - b₁) + 1) & (((b₄ - b₅) + 1) - b₁) + 1 = (((b₄ -' b₅) + 1) -' b₁) + 1 )

proof end;

theorem Th26: :: JORDAN4:26

for b₁ being Nat
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₃ & 1 <= b₁ & b₁ <= (b₅ -' b₄) + 1 holds
( (mid b₃,b₄,b₅) . b₁ = (mid b₃,b₅,b₄) . ((((b₅ - b₄) + 1) - b₁) + 1) & (((b₅ - b₄) + 1) - b₁) + 1 = (((b₅ -' b₄) + 1) -' b₁) + 1 )

proof end;

theorem Th27: :: JORDAN4:27

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;

theorem Th28: :: JORDAN4:28

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

proof end;

theorem Th29: :: JORDAN4:29

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;

theorem Th30: :: JORDAN4:30

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;

theorem Th31: :: JORDAN4:31

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃, b₄ being Nat st 1 <= b₂ & b₂ < b₃ & b₃ <= len b₁ & 1 <= b₄ & b₄ < (b₃ -' b₂) + 1 holds
LSeg (mid b₁,b₂,b₃),b₄ = LSeg b₁,((b₄ + b₂) -' 1)

proof end;

theorem Th32: :: JORDAN4:32

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃, b₄ being Nat st 1 <= b₂ & b₂ < b₃ & b₃ <= len b₁ & 1 <= b₄ & b₄ < (b₃ -' b₂) + 1 holds
LSeg (mid b₁,b₃,b₂),b₄ = LSeg b₁,(b₃ -' b₄)

proof end;

definition

let c₁ be Nat;
let c₂ be FinSequence;
func S_Drop c₁,c₂ -> Nat equals :Def1: :: JORDAN4:def 1
a₁ mod ((len a₂) -' 1) if a₁ mod ((len a₂) -' 1) <> 0
otherwise (len a₂) -' 1;
correctness ;

end;

:: deftheorem Def1 defines S_Drop JORDAN4:def 1 :

theorem Th33: :: JORDAN4:33

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

proof end;

theorem Th34: :: JORDAN4:34

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

proof end;

theorem Th35: :: JORDAN4:35

for b₁ being Nat
for b₂ being FinSequence holds
( S_Drop b₁,b₂ = S_Drop (b₁ + ((len b₂) -' 1)),b₂ & S_Drop b₁,b₂ = S_Drop (((len b₂) -' 1) + b₁),b₂ )

proof end;

definition

let c₁ be non constant standard special_circular_sequence;
let c₂ be FinSequence of (TOP-REAL 2);
let c₃, c₄ be Nat;
pred c₂ is_a_part>_of c₁,c₃,c₄ means :Def2: :: JORDAN4:def 2
( 1 <= a₃ & a₃ + 1 <= len a₁ & 1 <= a₄ & a₄ + 1 <= len a₁ & a₂ . (len a₂) = a₁ . a₄ & 1 <= len a₂ & len a₂ < len a₁ & ( for b₁ being Nat st 1 <= b₁ & b₁ <= len a₂ holds
a₂ . b₁ = a₁ . (S_Drop ((a₃ + b₁) -' 1),a₁) ) );

end;

:: deftheorem Def2 defines is_a_part>_of JORDAN4:def 2 :

definition

let c₁ be non constant standard special_circular_sequence;
let c₂ be FinSequence of (TOP-REAL 2);
let c₃, c₄ be Nat;
pred c₂ is_a_part<_of c₁,c₃,c₄ means :Def3: :: JORDAN4:def 3
( 1 <= a₃ & a₃ + 1 <= len a₁ & 1 <= a₄ & a₄ + 1 <= len a₁ & a₂ . (len a₂) = a₁ . a₄ & 1 <= len a₂ & len a₂ < len a₁ & ( for b₁ being Nat st 1 <= b₁ & b₁ <= len a₂ holds
a₂ . b₁ = a₁ . (S_Drop (((len a₁) + a₃) -' b₁),a₁) ) );

end;

:: deftheorem Def3 defines is_a_part<_of JORDAN4:def 3 :

definition

let c₁ be non constant standard special_circular_sequence;
let c₂ be FinSequence of (TOP-REAL 2);
let c₃, c₄ be Nat;
pred c₂ is_a_part_of c₁,c₃,c₄ means :Def4: :: JORDAN4:def 4
( a₂ is_a_part>_of a₁,a₃,a₄ or a₂ is_a_part<_of a₁,a₃,a₄ );

end;

:: deftheorem Def4 defines is_a_part_of JORDAN4:def 4 :

theorem Th36: :: JORDAN4:36

for b₁ being non constant standard special_circular_sequence
for b₂ being FinSequence of (TOP-REAL 2)
for b₃, b₄ being Nat st b₂ is_a_part_of b₁,b₃,b₄ holds
( 1 <= b₃ & b₃ + 1 <= len b₁ & 1 <= b₄ & b₄ + 1 <= len b₁ & b₂ . (len b₂) = b₁ . b₄ & 1 <= len b₂ & len b₂ < len b₁ & ( for b₅ being Nat st 1 <= b₅ & b₅ <= len b₂ holds
b₂ . b₅ = b₁ . (S_Drop ((b₃ + b₅) -' 1),b₁) or for b₅ being Nat st 1 <= b₅ & b₅ <= len b₂ holds
b₂ . b₅ = b₁ . (S_Drop (((len b₁) + b₃) -' b₅),b₁) ) )

proof end;

theorem Th37: :: JORDAN4:37

for b₁ being non constant standard special_circular_sequence
for b₂ being FinSequence of (TOP-REAL 2)
for b₃, b₄ being Nat st b₂ is_a_part>_of b₁,b₃,b₄ & b₃ <= b₄ holds
( len b₂ = (b₄ -' b₃) + 1 & b₂ = mid b₁,b₃,b₄ )

proof end;

theorem Th38: :: JORDAN4:38

for b₁ being non constant standard special_circular_sequence
for b₂ being FinSequence of (TOP-REAL 2)
for b₃, b₄ being Nat st b₂ is_a_part>_of b₁,b₃,b₄ & b₃ > b₄ holds
( len b₂ = ((len b₁) + b₄) -' b₃ & b₂ = (mid b₁,b₃,((len b₁) -' 1)) ^ (b₁ | b₄) & b₂ = (mid b₁,b₃,((len b₁) -' 1)) ^ (mid b₁,1,b₄) )

proof end;

theorem Th39: :: JORDAN4:39

for b₁ being non constant standard special_circular_sequence
for b₂ being FinSequence of (TOP-REAL 2)
for b₃, b₄ being Nat st b₂ is_a_part<_of b₁,b₃,b₄ & b₃ >= b₄ holds
( len b₂ = (b₃ -' b₄) + 1 & b₂ = mid b₁,b₃,b₄ )

proof end;

theorem Th40: :: JORDAN4:40

for b₁ being non constant standard special_circular_sequence
for b₂ being FinSequence of (TOP-REAL 2)
for b₃, b₄ being Nat st b₂ is_a_part<_of b₁,b₃,b₄ & b₃ < b₄ holds
( len b₂ = ((len b₁) + b₃) -' b₄ & b₂ = (mid b₁,b₃,1) ^ (mid b₁,((len b₁) -' 1),b₄) )

proof end;

theorem Th41: :: JORDAN4:41

for b₁ being non constant standard special_circular_sequence
for b₂ being FinSequence of (TOP-REAL 2)
for b₃, b₄ being Nat st b₂ is_a_part>_of b₁,b₃,b₄ holds
Rev b₂ is_a_part<_of b₁,b₄,b₃

proof end;

theorem Th42: :: JORDAN4:42

for b₁ being non constant standard special_circular_sequence
for b₂ being FinSequence of (TOP-REAL 2)
for b₃, b₄ being Nat st b₂ is_a_part<_of b₁,b₃,b₄ holds
Rev b₂ is_a_part>_of b₁,b₄,b₃

proof end;

theorem Th43: :: JORDAN4:43

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being Nat st 1 <= b₂ & b₂ <= b₃ & b₃ < len b₁ holds
mid b₁,b₂,b₃ is_a_part>_of b₁,b₂,b₃

proof end;

theorem Th44: :: JORDAN4:44

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being Nat st 1 <= b₂ & b₂ <= b₃ & b₃ < len b₁ holds
mid b₁,b₃,b₂ is_a_part<_of b₁,b₃,b₂

proof end;

theorem Th45: :: JORDAN4:45

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being Nat st 1 <= b₃ & b₂ > b₃ & b₂ < len b₁ holds
(mid b₁,b₂,((len b₁) -' 1)) ^ (mid b₁,1,b₃) is_a_part>_of b₁,b₂,b₃

proof end;

theorem Th46: :: JORDAN4:46

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being Nat st 1 <= b₂ & b₂ < b₃ & b₃ < len b₁ holds
(mid b₁,b₂,1) ^ (mid b₁,((len b₁) -' 1),b₃) is_a_part<_of b₁,b₂,b₃

proof end;

theorem Th47: :: JORDAN4:47

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;

theorem Th48: :: JORDAN4:48

for b₁ being non empty set
for b₂ being FinSequence of b₁ holds
( b₂ is one-to-one iff for b₃, b₄ being Nat st 1 <= b₃ & b₃ <= len b₂ & 1 <= b₄ & b₄ <= len b₂ & ( b₂ . b₃ = b₂ . b₄ or b₂ /. b₃ = b₂ /. b₄ ) holds
b₃ = b₄ )

proof end;

theorem Th49: :: JORDAN4:49

for b₁ being non constant standard special_circular_sequence
for b₂ being Nat st 1 < b₂ & b₂ + 1 <= len b₁ holds
b₁ | b₂ is_S-Seq

proof end;

theorem Th50: :: JORDAN4:50

for b₁ being non constant standard special_circular_sequence
for b₂ being Nat st 1 <= b₂ & b₂ + 1 < len b₁ holds
b₁ /^ b₂ is_S-Seq

proof end;

theorem Th51: :: JORDAN4:51

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being Nat st 1 <= b₂ & b₂ < b₃ & b₃ + 1 <= len b₁ holds
mid b₁,b₂,b₃ is_S-Seq

proof end;

theorem Th52: :: JORDAN4:52

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being Nat st 1 < b₂ & b₂ < b₃ & b₃ <= len b₁ holds
mid b₁,b₂,b₃ is_S-Seq

proof end;

theorem Th53: :: JORDAN4:53

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

proof end;

theorem Th54: :: JORDAN4:54

for b₁ being non constant standard special_circular_sequence holds (LSeg b₁,1) /\ (LSeg b₁,((len b₁) -' 1)) = {(b₁ . 1)}

proof end;

theorem Th55: :: JORDAN4:55

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being Nat
for b₄, b₅ being FinSequence of (TOP-REAL 2) st 1 <= b₂ & b₂ < b₃ & b₃ < len b₁ & b₄ = mid b₁,b₂,b₃ & b₅ = (mid b₁,b₂,1) ^ (mid b₁,((len b₁) -' 1),b₃) holds
( (L~ b₄) /\ (L~ b₅) = {(b₁ . b₂),(b₁ . b₃)} & (L~ b₄) \/ (L~ b₅) = L~ b₁ )

proof end;

theorem Th56: :: JORDAN4:56

for b₁ being non constant standard special_circular_sequence
for b₂ being FinSequence of (TOP-REAL 2)
for b₃, b₄ being Nat st b₂ is_a_part>_of b₁,b₃,b₄ & b₃ < b₄ holds
L~ b₂ is_S-P_arc_joining b₁ /. b₃,b₁ /. b₄

proof end;

Lemma51: for b₁ being non constant standard special_circular_sequence
for b₂ being FinSequence of (TOP-REAL 2)
for b₃, b₄ being Nat st b₂ is_a_part>_of b₁,b₃,b₄ & b₃ > b₄ holds
L~ b₂ is_S-P_arc_joining b₁ /. b₃,b₁ /. b₄

proof end;

theorem Th57: :: JORDAN4:57

for b₁ being non constant standard special_circular_sequence
for b₂ being FinSequence of (TOP-REAL 2)
for b₃, b₄ being Nat st b₂ is_a_part<_of b₁,b₃,b₄ & b₃ > b₄ holds
L~ b₂ is_S-P_arc_joining b₁ /. b₃,b₁ /. b₄

proof end;

theorem Th58: :: JORDAN4:58

for b₁ being non constant standard special_circular_sequence
for b₂ being FinSequence of (TOP-REAL 2)
for b₃, b₄ being Nat st b₂ is_a_part>_of b₁,b₃,b₄ & b₃ <> b₄ holds
L~ b₂ is_S-P_arc_joining b₁ /. b₃,b₁ /. b₄

proof end;

theorem Th59: :: JORDAN4:59

for b₁ being non constant standard special_circular_sequence
for b₂ being FinSequence of (TOP-REAL 2)
for b₃, b₄ being Nat st b₂ is_a_part<_of b₁,b₃,b₄ & b₃ <> b₄ holds
L~ b₂ is_S-P_arc_joining b₁ /. b₃,b₁ /. b₄

proof end;

theorem Th60: :: JORDAN4:60

for b₁ being non constant standard special_circular_sequence
for b₂ being FinSequence of (TOP-REAL 2)
for b₃, b₄ being Nat st b₂ is_a_part_of b₁,b₃,b₄ & b₃ <> b₄ holds
L~ b₂ is_S-P_arc_joining b₁ /. b₃,b₁ /. b₄

proof end;

theorem Th61: :: JORDAN4:61

for b₁ being non constant standard special_circular_sequence
for b₂ being FinSequence of (TOP-REAL 2)
for b₃, b₄ being Nat st b₂ is_a_part_of b₁,b₃,b₄ & b₂ . 1 <> b₂ . (len b₂) holds
L~ b₂ is_S-P_arc_joining b₁ /. b₃,b₁ /. b₄

proof end;

theorem Th62: :: JORDAN4:62

for b₁ being non constant standard special_circular_sequence
for b₂, b₃ being Nat st 1 <= b₂ & b₂ + 1 <= len b₁ & 1 <= b₃ & b₃ + 1 <= len b₁ & b₂ <> b₃ holds
ex b₄, b₅ being FinSequence of (TOP-REAL 2) st
( b₄ is_a_part_of b₁,b₂,b₃ & b₅ is_a_part_of b₁,b₂,b₃ & (L~ b₄) /\ (L~ b₅) = {(b₁ . b₂),(b₁ . b₃)} & (L~ b₄) \/ (L~ b₅) = L~ b₁ & L~ b₄ is_S-P_arc_joining b₁ /. b₂,b₁ /. b₃ & L~ b₅ is_S-P_arc_joining b₁ /. b₂,b₁ /. b₃ & ( for b₆ being FinSequence of (TOP-REAL 2) holds
( not b₆ is_a_part_of b₁,b₂,b₃ or b₆ = b₄ or b₆ = b₅ ) ) )

proof end;

theorem Th63: :: JORDAN4:63

for b₁ being non constant standard special_circular_sequence
for b₂ being non empty Subset of (TOP-REAL 2) st b₂ = L~ b₁ holds
b₂ is_simple_closed_curve

proof end;

theorem Th64: :: JORDAN4:64

for b₁, b₂ being Nat
for b₃ being non constant standard special_circular_sequence
for b₄, b₅ being FinSequence of (TOP-REAL 2) st b₄ is_a_part>_of b₃,b₁,b₂ & b₅ is_a_part>_of b₃,b₁,b₂ holds
b₄ = b₅

proof end;

theorem Th65: :: JORDAN4:65

for b₁, b₂ being Nat
for b₃ being non constant standard special_circular_sequence
for b₄, b₅ being FinSequence of (TOP-REAL 2) st b₄ is_a_part<_of b₃,b₁,b₂ & b₅ is_a_part<_of b₃,b₁,b₂ holds
b₄ = b₅

proof end;

theorem Th66: :: JORDAN4:66

for b₁, b₂ being Nat
for b₃ being non constant standard special_circular_sequence
for b₄, b₅ being FinSequence of (TOP-REAL 2) st b₁ <> b₂ & b₄ is_a_part>_of b₃,b₁,b₂ & b₅ is_a_part<_of b₃,b₁,b₂ holds
b₄ . 2 <> b₅ . 2

proof end;

theorem Th67: :: JORDAN4:67

for b₁, b₂ being Nat
for b₃ being non constant standard special_circular_sequence
for b₄, b₅ being FinSequence of (TOP-REAL 2) st b₁ <> b₂ & b₄ is_a_part_of b₃,b₁,b₂ & b₅ is_a_part_of b₃,b₁,b₂ & b₄ . 2 = b₅ . 2 holds
b₄ = b₅

proof end;

definition

let c₁ be non constant standard special_circular_sequence;
let c₂, c₃ be Nat;
assume E60: ( 1 <= c₂ & c₂ + 1 <= len c₁ & 1 <= c₃ & c₃ + 1 <= len c₁ & c₂ <> c₃ ) ;
func Lower c₁,c₂,c₃ -> FinSequence of (TOP-REAL 2) means :: JORDAN4:def 5
( a₄ is_a_part_of a₁,a₂,a₃ & ( ( (a₁ /. (a₂ + 1)) `1 < (a₁ /. a₂) `1 or (a₁ /. (a₂ + 1)) `2 < (a₁ /. a₂) `2 ) implies a₄ . 2 = a₁ . (a₂ + 1) ) & ( (a₁ /. (a₂ + 1)) `1 >= (a₁ /. a₂) `1 & (a₁ /. (a₂ + 1)) `2 >= (a₁ /. a₂) `2 implies a₄ . 2 = a₁ . (S_Drop (a₂ -' 1),a₁) ) );
correctness

proof end;

func Upper c₁,c₂,c₃ -> FinSequence of (TOP-REAL 2) means :: JORDAN4:def 6
( a₄ is_a_part_of a₁,a₂,a₃ & ( ( (a₁ /. (a₂ + 1)) `1 > (a₁ /. a₂) `1 or (a₁ /. (a₂ + 1)) `2 > (a₁ /. a₂) `2 ) implies a₄ . 2 = a₁ . (a₂ + 1) ) & ( (a₁ /. (a₂ + 1)) `1 <= (a₁ /. a₂) `1 & (a₁ /. (a₂ + 1)) `2 <= (a₁ /. a₂) `2 implies a₄ . 2 = a₁ . (S_Drop (a₂ -' 1),a₁) ) );
correctness

proof end;

end;

:: deftheorem Def5 defines Lower JORDAN4:def 5 :

:: deftheorem Def6 defines Upper JORDAN4:def 6 :