:: JORDAN1G semantic presentation

registration
cluster trivial set ;
existence
ex b1 being FinSequence st b1 is trivial
proof end;
end;

theorem Th1: :: JORDAN1G:1
for b1 being trivial FinSequence holds
( b1 is empty or ex b2 being set st b1 = <*b2*> )
proof end;

registration
let c1 be non trivial FinSequence;
cluster Rev a1 -> non trivial ;
coherence
not Rev c1 is trivial
proof end;
end;

theorem Th2: :: JORDAN1G:2
for b1 being non empty set
for b2 being FinSequence of b1
for b3 being Matrix of b1
for b4 being set st b2 is_sequence_on b3 holds
b2 -: b4 is_sequence_on b3
proof end;

theorem Th3: :: JORDAN1G:3
for b1 being non empty set
for b2 being FinSequence of b1
for b3 being Matrix of b1
for b4 being Element of b1 st b4 in rng b2 & b2 is_sequence_on b3 holds
b2 :- b4 is_sequence_on b3
proof end;

theorem Th4: :: JORDAN1G:4
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Upper_Seq b2,b1 is_sequence_on Gauge b2,b1
proof end;

theorem Th5: :: JORDAN1G:5
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Lower_Seq b2,b1 is_sequence_on Gauge b2,b1
proof end;

registration
let c1 be connected compact non horizontal non vertical Subset of (TOP-REAL 2);
let c2 be Nat;
cluster Upper_Seq a1,a2 -> standard ;
coherence
Upper_Seq c1,c2 is standard
proof end;
cluster Lower_Seq a1,a2 -> standard ;
coherence
Lower_Seq c1,c2 is standard
proof end;
end;

theorem Th6: :: JORDAN1G:6
for b1 being Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2)
for b2, b3, b4, b5 being Nat st [b2,b4] in Indices b1 & [b3,b5] in Indices b1 & (b1 * b2,b4) `2 = (b1 * b3,b5) `2 holds
b4 = b5
proof end;

theorem Th7: :: JORDAN1G:7
for b1 being X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2)
for b2, b3, b4, b5 being Nat st [b2,b4] in Indices b1 & [b3,b5] in Indices b1 & (b1 * b2,b4) `1 = (b1 * b3,b5) `1 holds
b2 = b3
proof end;

theorem Th8: :: JORDAN1G:8
canceled;

theorem Th9: :: JORDAN1G:9
canceled;

theorem Th10: :: JORDAN1G:10
canceled;

theorem Th11: :: JORDAN1G:11
canceled;

theorem Th12: :: JORDAN1G:12
canceled;

theorem Th13: :: JORDAN1G:13
canceled;

theorem Th14: :: JORDAN1G:14
canceled;

theorem Th15: :: JORDAN1G:15
canceled;

theorem Th16: :: JORDAN1G:16
for b1 being non trivial special unfolded standard FinSequence of (TOP-REAL 2) st ( ( b1 /. 1 <> N-min (L~ b1) & b1 /. (len b1) <> N-min (L~ b1) ) or ( b1 /. 1 <> N-max (L~ b1) & b1 /. (len b1) <> N-max (L~ b1) ) ) holds
(N-min (L~ b1)) `1 < (N-max (L~ b1)) `1
proof end;

theorem Th17: :: JORDAN1G:17
for b1 being non trivial special unfolded standard FinSequence of (TOP-REAL 2) st ( ( b1 /. 1 <> N-min (L~ b1) & b1 /. (len b1) <> N-min (L~ b1) ) or ( b1 /. 1 <> N-max (L~ b1) & b1 /. (len b1) <> N-max (L~ b1) ) ) holds
N-min (L~ b1) <> N-max (L~ b1)
proof end;

theorem Th18: :: JORDAN1G:18
for b1 being non trivial special unfolded standard FinSequence of (TOP-REAL 2) st ( ( b1 /. 1 <> S-min (L~ b1) & b1 /. (len b1) <> S-min (L~ b1) ) or ( b1 /. 1 <> S-max (L~ b1) & b1 /. (len b1) <> S-max (L~ b1) ) ) holds
(S-min (L~ b1)) `1 < (S-max (L~ b1)) `1
proof end;

theorem Th19: :: JORDAN1G:19
for b1 being non trivial special unfolded standard FinSequence of (TOP-REAL 2) st ( ( b1 /. 1 <> S-min (L~ b1) & b1 /. (len b1) <> S-min (L~ b1) ) or ( b1 /. 1 <> S-max (L~ b1) & b1 /. (len b1) <> S-max (L~ b1) ) ) holds
S-min (L~ b1) <> S-max (L~ b1)
proof end;

theorem Th20: :: JORDAN1G:20
for b1 being non trivial special unfolded standard FinSequence of (TOP-REAL 2) st ( ( b1 /. 1 <> W-min (L~ b1) & b1 /. (len b1) <> W-min (L~ b1) ) or ( b1 /. 1 <> W-max (L~ b1) & b1 /. (len b1) <> W-max (L~ b1) ) ) holds
(W-min (L~ b1)) `2 < (W-max (L~ b1)) `2
proof end;

theorem Th21: :: JORDAN1G:21
for b1 being non trivial special unfolded standard FinSequence of (TOP-REAL 2) st ( ( b1 /. 1 <> W-min (L~ b1) & b1 /. (len b1) <> W-min (L~ b1) ) or ( b1 /. 1 <> W-max (L~ b1) & b1 /. (len b1) <> W-max (L~ b1) ) ) holds
W-min (L~ b1) <> W-max (L~ b1)
proof end;

theorem Th22: :: JORDAN1G:22
for b1 being non trivial special unfolded standard FinSequence of (TOP-REAL 2) st ( ( b1 /. 1 <> E-min (L~ b1) & b1 /. (len b1) <> E-min (L~ b1) ) or ( b1 /. 1 <> E-max (L~ b1) & b1 /. (len b1) <> E-max (L~ b1) ) ) holds
(E-min (L~ b1)) `2 < (E-max (L~ b1)) `2
proof end;

theorem Th23: :: JORDAN1G:23
for b1 being non trivial special unfolded standard FinSequence of (TOP-REAL 2) st ( ( b1 /. 1 <> E-min (L~ b1) & b1 /. (len b1) <> E-min (L~ b1) ) or ( b1 /. 1 <> E-max (L~ b1) & b1 /. (len b1) <> E-max (L~ b1) ) ) holds
E-min (L~ b1) <> E-max (L~ b1)
proof end;

theorem Th24: :: JORDAN1G:24
for b1 being non empty set
for b2 being FinSequence of b1
for b3, b4 being Element of b1 st b3 in rng b2 & b4 in rng b2 & b4 .. b2 <= b3 .. b2 holds
(b2 -: b3) :- b4 = (b2 :- b4) -: b3
proof end;

theorem Th25: :: JORDAN1G:25
for b1 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat holds (L~ ((Cage b1,b2) -: (W-min (L~ (Cage b1,b2))))) /\ (L~ ((Cage b1,b2) :- (W-min (L~ (Cage b1,b2))))) = {(N-min (L~ (Cage b1,b2))),(W-min (L~ (Cage b1,b2)))}
proof end;

theorem Th26: :: JORDAN1G:26
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Lower_Seq b2,b1 = (Rotate (Cage b2,b1),(E-max (L~ (Cage b2,b1)))) -: (W-min (L~ (Cage b2,b1)))
proof end;

theorem Th27: :: JORDAN1G:27
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-min (L~ (Cage b2,b1))) .. (Upper_Seq b2,b1) = 1
proof end;

theorem Th28: :: JORDAN1G:28
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-min (L~ (Cage b2,b1))) .. (Upper_Seq b2,b1) < (W-max (L~ (Cage b2,b1))) .. (Upper_Seq b2,b1)
proof end;

theorem Th29: :: JORDAN1G:29
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-max (L~ (Cage b2,b1))) .. (Upper_Seq b2,b1) <= (N-min (L~ (Cage b2,b1))) .. (Upper_Seq b2,b1)
proof end;

theorem Th30: :: JORDAN1G:30
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (N-min (L~ (Cage b2,b1))) .. (Upper_Seq b2,b1) < (N-max (L~ (Cage b2,b1))) .. (Upper_Seq b2,b1)
proof end;

theorem Th31: :: JORDAN1G:31
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (N-max (L~ (Cage b2,b1))) .. (Upper_Seq b2,b1) <= (E-max (L~ (Cage b2,b1))) .. (Upper_Seq b2,b1)
proof end;

theorem Th32: :: JORDAN1G:32
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-max (L~ (Cage b2,b1))) .. (Upper_Seq b2,b1) = len (Upper_Seq b2,b1)
proof end;

theorem Th33: :: JORDAN1G:33
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-max (L~ (Cage b2,b1))) .. (Lower_Seq b2,b1) = 1
proof end;

theorem Th34: :: JORDAN1G:34
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-max (L~ (Cage b2,b1))) .. (Lower_Seq b2,b1) < (E-min (L~ (Cage b2,b1))) .. (Lower_Seq b2,b1)
proof end;

theorem Th35: :: JORDAN1G:35
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-min (L~ (Cage b2,b1))) .. (Lower_Seq b2,b1) <= (S-max (L~ (Cage b2,b1))) .. (Lower_Seq b2,b1)
proof end;

theorem Th36: :: JORDAN1G:36
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (S-max (L~ (Cage b2,b1))) .. (Lower_Seq b2,b1) < (S-min (L~ (Cage b2,b1))) .. (Lower_Seq b2,b1)
proof end;

theorem Th37: :: JORDAN1G:37
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (S-min (L~ (Cage b2,b1))) .. (Lower_Seq b2,b1) <= (W-min (L~ (Cage b2,b1))) .. (Lower_Seq b2,b1)
proof end;

theorem Th38: :: JORDAN1G:38
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-min (L~ (Cage b2,b1))) .. (Lower_Seq b2,b1) = len (Lower_Seq b2,b1)
proof end;

theorem Th39: :: JORDAN1G:39
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds ((Upper_Seq b2,b1) /. 2) `1 = W-bound (L~ (Cage b2,b1))
proof end;

theorem Th40: :: JORDAN1G:40
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds ((Lower_Seq b2,b1) /. 2) `1 = E-bound (L~ (Cage b2,b1))
proof end;

theorem Th41: :: JORDAN1G:41
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-bound (L~ (Cage b2,b1))) + (E-bound (L~ (Cage b2,b1))) = (W-bound b2) + (E-bound b2)
proof end;

theorem Th42: :: JORDAN1G:42
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (S-bound (L~ (Cage b2,b1))) + (N-bound (L~ (Cage b2,b1))) = (S-bound b2) + (N-bound b2)
proof end;

theorem Th43: :: JORDAN1G:43
for b1 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2, b3 being Nat st 1 <= b3 & b3 <= width (Gauge b1,b2) & b2 > 0 holds
((Gauge b1,b2) * (Center (Gauge b1,b2)),b3) `1 = ((W-bound b1) + (E-bound b1)) / 2
proof end;

theorem Th44: :: JORDAN1G:44
for b1 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2, b3 being Nat st 1 <= b3 & b3 <= len (Gauge b1,b2) & b2 > 0 holds
((Gauge b1,b2) * b3,(Center (Gauge b1,b2))) `2 = ((S-bound b1) + (N-bound b1)) / 2
proof end;

theorem Th45: :: JORDAN1G:45
for b1 being S-Sequence_in_R2
for b2, b3 being Nat st 1 <= b2 & b2 <= len b1 & 1 <= b3 & b3 <= len b1 & b1 /. 1 in L~ (mid b1,b2,b3) & not b2 = 1 holds
b3 = 1
proof end;

theorem Th46: :: JORDAN1G:46
for b1 being S-Sequence_in_R2
for b2, b3 being Nat st 1 <= b2 & b2 <= len b1 & 1 <= b3 & b3 <= len b1 & b1 /. (len b1) in L~ (mid b1,b2,b3) & not b2 = len b1 holds
b3 = len b1
proof end;

theorem Th47: :: JORDAN1G:47
for b1 being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat holds
( rng (Upper_Seq b1,b2) c= rng (Cage b1,b2) & rng (Lower_Seq b1,b2) c= rng (Cage b1,b2) )
proof end;

theorem Th48: :: JORDAN1G:48
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Upper_Seq b2,b1 is_a_h.c._for Cage b2,b1
proof end;

theorem Th49: :: JORDAN1G:49
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Rev (Lower_Seq b2,b1) is_a_h.c._for Cage b2,b1
proof end;

theorem Th50: :: JORDAN1G:50
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3 being Nat st 1 < b3 & b3 <= len (Gauge b2,b1) holds
not (Gauge b2,b1) * b3,1 in rng (Upper_Seq b2,b1)
proof end;

theorem Th51: :: JORDAN1G:51
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3 being Nat st 1 <= b3 & b3 < len (Gauge b2,b1) holds
not (Gauge b2,b1) * b3,(width (Gauge b2,b1)) in rng (Lower_Seq b2,b1)
proof end;

theorem Th52: :: JORDAN1G:52
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3 being Nat st 1 < b3 & b3 <= len (Gauge b2,b1) holds
not (Gauge b2,b1) * b3,1 in L~ (Upper_Seq b2,b1)
proof end;

theorem Th53: :: JORDAN1G:53
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3 being Nat st 1 <= b3 & b3 < len (Gauge b2,b1) holds
not (Gauge b2,b1) * b3,(width (Gauge b2,b1)) in L~ (Lower_Seq b2,b1)
proof end;

theorem Th54: :: JORDAN1G:54
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4 being Nat st 1 <= b3 & b3 <= len (Gauge b2,b1) & 1 <= b4 & b4 <= width (Gauge b2,b1) & (Gauge b2,b1) * b3,b4 in L~ (Cage b2,b1) holds
LSeg ((Gauge b2,b1) * b3,1),((Gauge b2,b1) * b3,b4) meets L~ (Lower_Seq b2,b1)
proof end;

theorem Th55: :: JORDAN1G:55
for b1 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat st b2 > 0 holds
First_Point (L~ (Upper_Seq b1,b2)),(W-min (L~ (Cage b1,b2))),(E-max (L~ (Cage b1,b2))),(Vertical_Line (((W-bound (L~ (Cage b1,b2))) + (E-bound (L~ (Cage b1,b2)))) / 2)) in rng (Upper_Seq b1,b2)
proof end;

theorem Th56: :: JORDAN1G:56
for b1 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat st b2 > 0 holds
Last_Point (L~ (Lower_Seq b1,b2)),(E-max (L~ (Cage b1,b2))),(W-min (L~ (Cage b1,b2))),(Vertical_Line (((W-bound (L~ (Cage b1,b2))) + (E-bound (L~ (Cage b1,b2)))) / 2)) in rng (Lower_Seq b1,b2)
proof end;

theorem Th57: :: JORDAN1G:57
for b1 being S-Sequence_in_R2
for b2 being Point of (TOP-REAL 2) st b2 in rng b1 holds
R_Cut b1,b2 = mid b1,1,(b2 .. b1)
proof end;

theorem Th58: :: JORDAN1G:58
for b1 being S-Sequence_in_R2
for b2 being closed Subset of (TOP-REAL 2) st L~ b1 meets b2 & not b1 /. 1 in b2 & First_Point (L~ b1),(b1 /. 1),(b1 /. (len b1)),b2 in rng b1 holds
(L~ (mid b1,1,((First_Point (L~ b1),(b1 /. 1),(b1 /. (len b1)),b2) .. b1))) /\ b2 = {(First_Point (L~ b1),(b1 /. 1),(b1 /. (len b1)),b2)}
proof end;

theorem Th59: :: JORDAN1G:59
for b1 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat st b2 > 0 holds
for b3 being Nat st 1 <= b3 & b3 < (First_Point (L~ (Upper_Seq b1,b2)),(W-min (L~ (Cage b1,b2))),(E-max (L~ (Cage b1,b2))),(Vertical_Line (((W-bound (L~ (Cage b1,b2))) + (E-bound (L~ (Cage b1,b2)))) / 2))) .. (Upper_Seq b1,b2) holds
((Upper_Seq b1,b2) /. b3) `1 < ((W-bound (L~ (Cage b1,b2))) + (E-bound (L~ (Cage b1,b2)))) / 2
proof end;

theorem Th60: :: JORDAN1G:60
for b1 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat st b2 > 0 holds
for b3 being Nat st 1 <= b3 & b3 < (First_Point (L~ (Rev (Lower_Seq b1,b2))),(W-min (L~ (Cage b1,b2))),(E-max (L~ (Cage b1,b2))),(Vertical_Line (((W-bound (L~ (Cage b1,b2))) + (E-bound (L~ (Cage b1,b2)))) / 2))) .. (Rev (Lower_Seq b1,b2)) holds
((Rev (Lower_Seq b1,b2)) /. b3) `1 < ((W-bound (L~ (Cage b1,b2))) + (E-bound (L~ (Cage b1,b2)))) / 2
proof end;

theorem Th61: :: JORDAN1G:61
for b1 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat st b2 > 0 holds
for b3 being Point of (TOP-REAL 2) st b3 in rng (mid (Upper_Seq b1,b2),2,((First_Point (L~ (Upper_Seq b1,b2)),(W-min (L~ (Cage b1,b2))),(E-max (L~ (Cage b1,b2))),(Vertical_Line (((W-bound (L~ (Cage b1,b2))) + (E-bound (L~ (Cage b1,b2)))) / 2))) .. (Upper_Seq b1,b2))) holds
b3 `1 <= ((W-bound (L~ (Cage b1,b2))) + (E-bound (L~ (Cage b1,b2)))) / 2
proof end;

theorem Th62: :: JORDAN1G:62
for b1 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat st b2 > 0 holds
(First_Point (L~ (Upper_Seq b1,b2)),(W-min (L~ (Cage b1,b2))),(E-max (L~ (Cage b1,b2))),(Vertical_Line (((W-bound (L~ (Cage b1,b2))) + (E-bound (L~ (Cage b1,b2)))) / 2))) `2 > (Last_Point (L~ (Lower_Seq b1,b2)),(E-max (L~ (Cage b1,b2))),(W-min (L~ (Cage b1,b2))),(Vertical_Line (((W-bound (L~ (Cage b1,b2))) + (E-bound (L~ (Cage b1,b2)))) / 2))) `2
proof end;

theorem Th63: :: JORDAN1G:63
for b1 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat st b2 > 0 holds
L~ (Upper_Seq b1,b2) = Upper_Arc (L~ (Cage b1,b2))
proof end;

theorem Th64: :: JORDAN1G:64
for b1 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat st b2 > 0 holds
L~ (Lower_Seq b1,b2) = Lower_Arc (L~ (Cage b1,b2))
proof end;

theorem Th65: :: JORDAN1G:65
for b1 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat st b2 > 0 holds
for b3, b4 being Nat st 1 <= b3 & b3 <= len (Gauge b1,b2) & 1 <= b4 & b4 <= width (Gauge b1,b2) & (Gauge b1,b2) * b3,b4 in L~ (Cage b1,b2) holds
LSeg ((Gauge b1,b2) * b3,1),((Gauge b1,b2) * b3,b4) meets Lower_Arc (L~ (Cage b1,b2))
proof end;