:: JORDAN1J semantic presentation

theorem Th1: :: JORDAN1J:1
for b1 being Go-board
for b2, b3, b4, b5 being Nat st 1 <= b4 & b4 <= width b1 & 1 <= b5 & b5 <= width b1 & 1 <= b2 & b2 < b3 & b3 <= len b1 holds
(b1 * b2,b4) `1 < (b1 * b3,b5) `1
proof end;

theorem Th2: :: JORDAN1J:2
for b1 being Go-board
for b2, b3, b4, b5 being Nat st 1 <= b2 & b2 <= len b1 & 1 <= b3 & b3 <= len b1 & 1 <= b4 & b4 < b5 & b5 <= width b1 holds
(b1 * b2,b4) `2 < (b1 * b3,b5) `2
proof end;

registration
let c1 be non empty FinSequence;
let c2 be FinSequence;
cluster a1 ^' a2 -> non empty ;
coherence
not c1 ^' c2 is empty
proof end;
end;

theorem Th3: :: JORDAN1J:3
for b1 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat holds (L~ ((Cage b1,b2) -: (E-max (L~ (Cage b1,b2))))) /\ (L~ ((Cage b1,b2) :- (E-max (L~ (Cage b1,b2))))) = {(N-min (L~ (Cage b1,b2))),(E-max (L~ (Cage b1,b2)))}
proof end;

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

theorem Th5: :: JORDAN1J:5
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( W-min (L~ (Cage b2,b1)) in rng (Upper_Seq b2,b1) & W-min (L~ (Cage b2,b1)) in L~ (Upper_Seq b2,b1) )
proof end;

theorem Th6: :: JORDAN1J:6
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( W-max (L~ (Cage b2,b1)) in rng (Upper_Seq b2,b1) & W-max (L~ (Cage b2,b1)) in L~ (Upper_Seq b2,b1) )
proof end;

theorem Th7: :: JORDAN1J:7
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( N-min (L~ (Cage b2,b1)) in rng (Upper_Seq b2,b1) & N-min (L~ (Cage b2,b1)) in L~ (Upper_Seq b2,b1) )
proof end;

theorem Th8: :: JORDAN1J:8
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( N-max (L~ (Cage b2,b1)) in rng (Upper_Seq b2,b1) & N-max (L~ (Cage b2,b1)) in L~ (Upper_Seq b2,b1) )
proof end;

theorem Th9: :: JORDAN1J:9
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( E-max (L~ (Cage b2,b1)) in rng (Upper_Seq b2,b1) & E-max (L~ (Cage b2,b1)) in L~ (Upper_Seq b2,b1) )
proof end;

theorem Th10: :: JORDAN1J:10
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( E-max (L~ (Cage b2,b1)) in rng (Lower_Seq b2,b1) & E-max (L~ (Cage b2,b1)) in L~ (Lower_Seq b2,b1) )
proof end;

theorem Th11: :: JORDAN1J:11
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( E-min (L~ (Cage b2,b1)) in rng (Lower_Seq b2,b1) & E-min (L~ (Cage b2,b1)) in L~ (Lower_Seq b2,b1) )
proof end;

theorem Th12: :: JORDAN1J:12
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( S-max (L~ (Cage b2,b1)) in rng (Lower_Seq b2,b1) & S-max (L~ (Cage b2,b1)) in L~ (Lower_Seq b2,b1) )
proof end;

theorem Th13: :: JORDAN1J:13
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( S-min (L~ (Cage b2,b1)) in rng (Lower_Seq b2,b1) & S-min (L~ (Cage b2,b1)) in L~ (Lower_Seq b2,b1) )
proof end;

theorem Th14: :: JORDAN1J:14
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( W-min (L~ (Cage b2,b1)) in rng (Lower_Seq b2,b1) & W-min (L~ (Cage b2,b1)) in L~ (Lower_Seq b2,b1) )
proof end;

theorem Th15: :: JORDAN1J:15
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st b1 c= b2 & N-min b2 in b1 holds
N-min b1 = N-min b2
proof end;

theorem Th16: :: JORDAN1J:16
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st b1 c= b2 & N-max b2 in b1 holds
N-max b1 = N-max b2
proof end;

theorem Th17: :: JORDAN1J:17
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st b1 c= b2 & E-min b2 in b1 holds
E-min b1 = E-min b2
proof end;

theorem Th18: :: JORDAN1J:18
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st b1 c= b2 & E-max b2 in b1 holds
E-max b1 = E-max b2
proof end;

theorem Th19: :: JORDAN1J:19
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st b1 c= b2 & S-min b2 in b1 holds
S-min b1 = S-min b2
proof end;

theorem Th20: :: JORDAN1J:20
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st b1 c= b2 & S-max b2 in b1 holds
S-max b1 = S-max b2
proof end;

theorem Th21: :: JORDAN1J:21
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st b1 c= b2 & W-min b2 in b1 holds
W-min b1 = W-min b2
proof end;

theorem Th22: :: JORDAN1J:22
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st b1 c= b2 & W-max b2 in b1 holds
W-max b1 = W-max b2
proof end;

theorem Th23: :: JORDAN1J:23
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st N-bound b1 <= N-bound b2 holds
N-bound (b1 \/ b2) = N-bound b2
proof end;

theorem Th24: :: JORDAN1J:24
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st E-bound b1 <= E-bound b2 holds
E-bound (b1 \/ b2) = E-bound b2
proof end;

theorem Th25: :: JORDAN1J:25
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st S-bound b1 <= S-bound b2 holds
S-bound (b1 \/ b2) = S-bound b1
proof end;

theorem Th26: :: JORDAN1J:26
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st W-bound b1 <= W-bound b2 holds
W-bound (b1 \/ b2) = W-bound b1
proof end;

theorem Th27: :: JORDAN1J:27
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st N-bound b1 < N-bound b2 holds
N-min (b1 \/ b2) = N-min b2
proof end;

theorem Th28: :: JORDAN1J:28
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st N-bound b1 < N-bound b2 holds
N-max (b1 \/ b2) = N-max b2
proof end;

theorem Th29: :: JORDAN1J:29
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st E-bound b1 < E-bound b2 holds
E-min (b1 \/ b2) = E-min b2
proof end;

theorem Th30: :: JORDAN1J:30
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st E-bound b1 < E-bound b2 holds
E-max (b1 \/ b2) = E-max b2
proof end;

theorem Th31: :: JORDAN1J:31
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st S-bound b1 < S-bound b2 holds
S-min (b1 \/ b2) = S-min b1
proof end;

theorem Th32: :: JORDAN1J:32
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st S-bound b1 < S-bound b2 holds
S-max (b1 \/ b2) = S-max b1
proof end;

theorem Th33: :: JORDAN1J:33
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st W-bound b1 < W-bound b2 holds
W-min (b1 \/ b2) = W-min b1
proof end;

theorem Th34: :: JORDAN1J:34
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st W-bound b1 < W-bound b2 holds
W-max (b1 \/ b2) = W-max b1
proof end;

theorem Th35: :: JORDAN1J:35
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b1 is_S-Seq & b2 in L~ b1 holds
(L_Cut b1,b2) /. (len (L_Cut b1,b2)) = b1 /. (len b1)
proof end;

theorem Th36: :: JORDAN1J:36
for b1 being non constant standard special_circular_sequence
for b2, b3 being Point of (TOP-REAL 2)
for b4 being connected Subset of (TOP-REAL 2) st b2 in RightComp b1 & b3 in LeftComp b1 & b2 in b4 & b3 in b4 holds
b4 meets L~ b1
proof end;

registration
cluster non constant being_S-Seq s.c.c. standard FinSequence of the carrier of (TOP-REAL 2);
existence
ex b1 being being_S-Seq FinSequence of (TOP-REAL 2) st
( not b1 is constant & b1 is standard & b1 is s.c.c. )
proof end;
end;

theorem Th37: :: JORDAN1J:37
for b1 being S-Sequence_in_R2
for b2 being Point of (TOP-REAL 2) st b2 in rng b1 holds
L_Cut b1,b2 = mid b1,(b2 .. b1),(len b1)
proof end;

theorem Th38: :: JORDAN1J:38
for b1 being Go-board
for b2 being S-Sequence_in_R2 st b2 is_sequence_on b1 holds
for b3 being Point of (TOP-REAL 2) st b3 in rng b2 holds
R_Cut b2,b3 is_sequence_on b1
proof end;

theorem Th39: :: JORDAN1J:39
for b1 being Go-board
for b2 being S-Sequence_in_R2 st b2 is_sequence_on b1 holds
for b3 being Point of (TOP-REAL 2) st b3 in rng b2 holds
L_Cut b2,b3 is_sequence_on b1
proof end;

theorem Th40: :: JORDAN1J:40
for b1 being Go-board
for b2 being FinSequence of (TOP-REAL 2) st b2 is_sequence_on b1 holds
for b3, b4 being Nat st 1 <= b3 & b3 <= len b1 & 1 <= b4 & b4 <= width b1 & b1 * b3,b4 in L~ b2 holds
b1 * b3,b4 in rng b2
proof end;

theorem Th41: :: JORDAN1J:41
for b1 being S-Sequence_in_R2
for b2 being FinSequence of (TOP-REAL 2) st b2 is unfolded & b2 is s.n.c. & b2 is one-to-one & (L~ b1) /\ (L~ b2) = {(b1 /. 1)} & b1 /. 1 = b2 /. (len b2) & ( for b3 being Nat st 1 <= b3 & b3 + 2 <= len b1 holds
(LSeg b1,b3) /\ (LSeg (b1 /. (len b1)),(b2 /. 1)) = {} ) & ( for b3 being Nat st 2 <= b3 & b3 + 1 <= len b2 holds
(LSeg b2,b3) /\ (LSeg (b1 /. (len b1)),(b2 /. 1)) = {} ) holds
b1 ^ b2 is s.c.c.
proof end;

theorem Th42: :: JORDAN1J:42
for b1 being Nat
for b2 being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) ex b3 being Nat st
( 1 <= b3 & b3 + 1 <= len (Gauge b2,b1) & W-min b2 in cell (Gauge b2,b1),1,b3 & W-min b2 <> (Gauge b2,b1) * 2,b3 )
proof end;

theorem Th43: :: JORDAN1J:43
for b1 being S-Sequence_in_R2
for b2 being Point of (TOP-REAL 2) st b2 in L~ b1 & b1 . (len b1) in L~ (R_Cut b1,b2) holds
b1 . (len b1) = b2
proof end;

theorem Th44: :: JORDAN1J:44
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) holds R_Cut b1,b2 <> {}
proof end;

theorem Th45: :: JORDAN1J:45
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b2 in L~ b1 holds
(R_Cut b1,b2) /. (len (R_Cut b1,b2)) = b2
proof end;

theorem Th46: :: JORDAN1J:46
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3 being Point of (TOP-REAL 2) st b3 in L~ (Upper_Seq b2,b1) & b3 `1 = E-bound (L~ (Cage b2,b1)) holds
b3 = E-max (L~ (Cage b2,b1))
proof end;

theorem Th47: :: JORDAN1J:47
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3 being Point of (TOP-REAL 2) st b3 in L~ (Lower_Seq b2,b1) & b3 `1 = W-bound (L~ (Cage b2,b1)) holds
b3 = W-min (L~ (Cage b2,b1))
proof end;

theorem Th48: :: JORDAN1J:48
for b1 being Go-board
for b2, b3 being FinSequence of (TOP-REAL 2)
for b4 being Nat st 1 <= b4 & b4 < len b2 & b2 ^ b3 is_sequence_on b1 holds
( left_cell (b2 ^ b3),b4,b1 = left_cell b2,b4,b1 & right_cell (b2 ^ b3),b4,b1 = right_cell b2,b4,b1 )
proof end;

theorem Th49: :: JORDAN1J:49
for b1 being set
for b2, b3 being FinSequence of b1
for b4 being Nat st b4 <= len b2 holds
(b2 ^' b3) | b4 = b2 | b4
proof end;

theorem Th50: :: JORDAN1J:50
for b1 being set
for b2, b3 being FinSequence of b1 holds (b2 ^' b3) | (len b2) = b2
proof end;

theorem Th51: :: JORDAN1J:51
for b1 being Go-board
for b2, b3 being FinSequence of (TOP-REAL 2)
for b4 being Nat st 1 <= b4 & b4 < len b2 & b2 ^' b3 is_sequence_on b1 holds
( left_cell (b2 ^' b3),b4,b1 = left_cell b2,b4,b1 & right_cell (b2 ^' b3),b4,b1 = right_cell b2,b4,b1 )
proof end;

theorem Th52: :: JORDAN1J:52
for b1 being Go-board
for b2 being S-Sequence_in_R2
for b3 being Point of (TOP-REAL 2)
for b4 being Nat st 1 <= b4 & b4 < b3 .. b2 & b2 is_sequence_on b1 & b3 in rng b2 holds
( left_cell (R_Cut b2,b3),b4,b1 = left_cell b2,b4,b1 & right_cell (R_Cut b2,b3),b4,b1 = right_cell b2,b4,b1 )
proof end;

theorem Th53: :: JORDAN1J:53
for b1 being Go-board
for b2 being FinSequence of (TOP-REAL 2)
for b3 being Point of (TOP-REAL 2)
for b4 being Nat st 1 <= b4 & b4 < b3 .. b2 & b2 is_sequence_on b1 holds
( left_cell (b2 -: b3),b4,b1 = left_cell b2,b4,b1 & right_cell (b2 -: b3),b4,b1 = right_cell b2,b4,b1 )
proof end;

theorem Th54: :: JORDAN1J:54
for b1, b2 being FinSequence of (TOP-REAL 2) st b1 is unfolded & b1 is s.n.c. & b1 is one-to-one & b2 is unfolded & b2 is s.n.c. & b2 is one-to-one & b1 /. (len b1) = b2 /. 1 & (L~ b1) /\ (L~ b2) = {(b2 /. 1)} holds
b1 ^' b2 is s.n.c.
proof end;

theorem Th55: :: JORDAN1J:55
for b1, b2 being FinSequence of (TOP-REAL 2) st b1 is one-to-one & b2 is one-to-one & (rng b1) /\ (rng b2) c= {(b2 /. 1)} holds
b1 ^' b2 is one-to-one
proof end;

theorem Th56: :: JORDAN1J:56
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b1 is_S-Seq & b2 in rng b1 & b2 <> b1 . 1 holds
(Index b2,b1) + 1 = b2 .. b1
proof end;

theorem Th57: :: JORDAN1J:57
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,b1) & 1 <= b4 & b5 <= width (Gauge b2,b1) & (Gauge b2,b1) * b3,b5 in L~ (Upper_Seq b2,b1) & (Gauge b2,b1) * b3,b4 in L~ (Lower_Seq b2,b1) holds
b4 <> b5
proof end;

theorem Th58: :: JORDAN1J:58
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & (LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5)) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b3,b5)} & (LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5)) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b3,b4)} holds
LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5) meets Lower_Arc b2
proof end;

theorem Th59: :: JORDAN1J:59
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & (LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5)) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b3,b5)} & (LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5)) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b3,b4)} holds
LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5) meets Upper_Arc b2
proof end;

theorem Th60: :: JORDAN1J:60
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & b1 > 0 & (LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5)) /\ (Upper_Arc (L~ (Cage b2,b1))) = {((Gauge b2,b1) * b3,b5)} & (LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5)) /\ (Lower_Arc (L~ (Cage b2,b1))) = {((Gauge b2,b1) * b3,b4)} holds
LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5) meets Lower_Arc b2
proof end;

theorem Th61: :: JORDAN1J:61
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & b1 > 0 & (LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5)) /\ (Upper_Arc (L~ (Cage b2,b1))) = {((Gauge b2,b1) * b3,b5)} & (LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5)) /\ (Lower_Arc (L~ (Cage b2,b1))) = {((Gauge b2,b1) * b3,b4)} holds
LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5) meets Upper_Arc b2
proof end;

theorem Th62: :: JORDAN1J:62
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3 being Nat st (Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b3 in Upper_Arc (L~ (Cage b2,(b1 + 1))) & 1 <= b3 & b3 <= width (Gauge b2,(b1 + 1)) holds
LSeg ((Gauge b2,1) * (Center (Gauge b2,1)),1),((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b3) meets Lower_Arc (L~ (Cage b2,(b1 + 1)))
proof end;

theorem Th63: :: JORDAN1J:63
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4 being Nat st 1 <= b3 & b3 <= b4 & b4 <= width (Gauge b2,(b1 + 1)) & (LSeg ((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b3),((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b4)) /\ (Upper_Arc (L~ (Cage b2,(b1 + 1)))) = {((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b4)} & (LSeg ((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b3),((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b4)) /\ (Lower_Arc (L~ (Cage b2,(b1 + 1)))) = {((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b3)} holds
LSeg ((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b3),((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b4) meets Lower_Arc b2
proof end;

theorem Th64: :: JORDAN1J:64
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4 being Nat st 1 <= b3 & b3 <= b4 & b4 <= width (Gauge b2,(b1 + 1)) & (LSeg ((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b3),((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b4)) /\ (Upper_Arc (L~ (Cage b2,(b1 + 1)))) = {((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b4)} & (LSeg ((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b3),((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b4)) /\ (Lower_Arc (L~ (Cage b2,(b1 + 1)))) = {((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b3)} holds
LSeg ((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b3),((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b4) meets Upper_Arc b2
proof end;