let n be Nat; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p in BDD (L~ (Cage (C,n))) holds
ex B being S-Sequence_in_R2 st
( B = B_Cut (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) & ex P being S-Sequence_in_R2 st
( P is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ P & P /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & P /. (len P) = South-Bound (p,(L~ (Cage (C,n)))) & len P >= 2 & ex B1 being S-Sequence_in_R2 st
( B1 is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ B = L~ B1 & B /. 1 = B1 /. 1 & B /. (len B) = B1 /. (len B1) & len B <= len B1 & ex g being constant standard special_circular_sequence st g = B1 ^' P ) ) )
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) st p in BDD (L~ (Cage (C,n))) holds
ex B being S-Sequence_in_R2 st
( B = B_Cut (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) & ex P being S-Sequence_in_R2 st
( P is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ P & P /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & P /. (len P) = South-Bound (p,(L~ (Cage (C,n)))) & len P >= 2 & ex B1 being S-Sequence_in_R2 st
( B1 is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ B = L~ B1 & B /. 1 = B1 /. 1 & B /. (len B) = B1 /. (len B1) & len B <= len B1 & ex g being constant standard special_circular_sequence st g = B1 ^' P ) ) )
let p, q be Point of (TOP-REAL 2); :: thesis: ( p in BDD (L~ (Cage (C,n))) implies ex B being S-Sequence_in_R2 st
( B = B_Cut (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) & ex P being S-Sequence_in_R2 st
( P is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ P & P /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & P /. (len P) = South-Bound (p,(L~ (Cage (C,n)))) & len P >= 2 & ex B1 being S-Sequence_in_R2 st
( B1 is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ B = L~ B1 & B /. 1 = B1 /. 1 & B /. (len B) = B1 /. (len B1) & len B <= len B1 & ex g being constant standard special_circular_sequence st g = B1 ^' P ) ) ) )
set f = Cage (C,n);
set Lf = L~ (Cage (C,n));
set a = North-Bound (p,(L~ (Cage (C,n))));
set b = South-Bound (p,(L~ (Cage (C,n))));
set Rotf = Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))));
set rf = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1);
A1: L~ (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) = L~ (Cage (C,n)) by REVROT_1:33;
A2: (LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1))) /\ (LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1)) = {((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)} by GOBOARD7:34, REVROT_1:30;
then A3: LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) meets LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) ;
A4: (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2 in LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)) by RLTOPSP1:68;
len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) >= 1 + 1 by GOBOARD7:34, XXREAL_0:2;
then A5: LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) = LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1))) by TOPREAL1:def 3;
A6: (South-Bound (p,(L~ (Cage (C,n))))) `1 = p `1 by JORDAN18:16;
len (Cage (C,n)) > 4 by GOBOARD7:34;
then A7: ((len (Cage (C,n))) -' 1) + 1 = len (Cage (C,n)) by XREAL_1:235, XXREAL_0:2;
then A8: (len (Cage (C,n))) -' 1 < len (Cage (C,n)) by NAT_1:13;
set pion = <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>;
A9: len (Cage (C,n)) > 1 by GOBOARD7:34, XXREAL_0:2;
A10: (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) in LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))))) by RLTOPSP1:68;
assume A11: p in BDD (L~ (Cage (C,n))) ; :: thesis: ex B being S-Sequence_in_R2 st
( B = B_Cut (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) & ex P being S-Sequence_in_R2 st
( P is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ P & P /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & P /. (len P) = South-Bound (p,(L~ (Cage (C,n)))) & len P >= 2 & ex B1 being S-Sequence_in_R2 st
( B1 is_sequence_on GoB (B ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ B = L~ B1 & B /. 1 = B1 /. 1 & B /. (len B) = B1 /. (len B1) & len B <= len B1 & ex g being constant standard special_circular_sequence st g = B1 ^' P ) ) )
A12: North-Bound (p,(L~ (Cage (C,n)))) <> South-Bound (p,(L~ (Cage (C,n)))) by A11, JORDAN18:20;
A13: South-Bound (p,(L~ (Cage (C,n)))) in L~ (Cage (C,n)) by A11, JORDAN18:17;
then A14: Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))) < len (Cage (C,n)) by JORDAN3:8;
A15: for i being Nat st 1 <= i & i < Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))) holds
(Cage (C,n)) /. i <> (Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))) by A14, GOBOARD7:36;
1 <= Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))) by A13, JORDAN3:8;
then A16: Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))) in dom (Cage (C,n)) by A14, FINSEQ_3:25;
then ((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n)) <= Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))) by FINSEQ_5:39;
then 0 + (((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n))) < len (Cage (C,n)) by A14, XXREAL_0:2;
then A17: (len (Cage (C,n))) - (((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n))) > 1 - 1 by XREAL_1:20;
A18: (Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))) in rng (Cage (C,n)) by A16, PARTFUN2:2;
then len ((Cage (C,n)) :- ((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))) = ((len (Cage (C,n))) - (((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n)))) + 1 by FINSEQ_5:50;
then 1 < len ((Cage (C,n)) :- ((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))) by A17, XREAL_1:19;
then A19: LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) = LSeg ((Cage (C,n)),((1 -' 1) + (((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n))))) by A18, REVROT_1:24
.= LSeg ((Cage (C,n)),(0 + (((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) .. (Cage (C,n))))) by XREAL_1:232
.= LSeg ((Cage (C,n)),(Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))) by A16, A15, FINSEQ_6:48 ;
then A20: South-Bound (p,(L~ (Cage (C,n)))) in LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) by A13, JORDAN3:9;
A21: len (Cage (C,n)) > 1 + 1 by GOBOARD7:34, XXREAL_0:2;
then A22: (len (Cage (C,n))) - 1 > 1 by XREAL_1:20;
then A23: 1 < (len (Cage (C,n))) -' 1 by XREAL_0:def 2;
A24: len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) = len (Cage (C,n)) by FINSEQ_6:179;
then A25: LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) = LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1))) by A21, TOPREAL1:def 3;
A26: (North-Bound (p,(L~ (Cage (C,n))))) `1 = p `1 by JORDAN18:16;
then LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))) is vertical by A6, SPPOL_1:16;
then A27: <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> is being_S-Seq by A12, JORDAN1B:7;
A28: p `2 < (North-Bound (p,(L~ (Cage (C,n))))) `2 by A11, JORDAN18:18;
A29: (South-Bound (p,(L~ (Cage (C,n))))) `2 < p `2 by A11, JORDAN18:18;
then A30: p in LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))) by A26, A6, A28, GOBOARD7:7;
A31: LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) = LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))))) by A24, A22, A7, TOPREAL1:def 3;
reconsider rf = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) as S-Sequence_in_R2 by A24, A22, A7, JORDAN4:37;
A32: L~ (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) = (L~ rf) \/ (LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1))) by A24, A22, A7, GOBOARD2:3;
A33: (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1 = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) by FINSEQ_6:def 1;
A34: (South-Bound (p,(L~ (Cage (C,n))))) `2 < (North-Bound (p,(L~ (Cage (C,n))))) `2 by A29, A28, XXREAL_0:2;
A35: now :: thesis: not North-Bound (p,(L~ (Cage (C,n)))) in LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1))
assume A36: North-Bound (p,(L~ (Cage (C,n)))) in LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) ; :: thesis: contradiction
per cases ( ( LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) is vertical & LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) is vertical ) or ( LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) is vertical & LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) is horizontal ) or ( LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) is horizontal & LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) is vertical ) or ( LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) is horizontal & LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) is horizontal ) ) by SPPOL_1:19;
suppose A37: ( LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) is vertical & LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) is vertical ) ; :: thesis: contradiction
then A38: (South-Bound (p,(L~ (Cage (C,n))))) `1 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1 by A13, A19, A25, JORDAN3:9, SPPOL_1:41;
A39: ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `1 by A25, A37, SPPOL_1:16;
A40: ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `1 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `1 by A31, A37, SPPOL_1:16;
per cases ( (South-Bound (p,(L~ (Cage (C,n))))) `2 < ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 or ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 < (North-Bound (p,(L~ (Cage (C,n))))) `2 ) by A34, XXREAL_0:2;
suppose A41: (South-Bound (p,(L~ (Cage (C,n))))) `2 < ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 ; :: thesis: contradiction
then A42: (((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2 < ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 by XREAL_1:226;
A43: (South-Bound (p,(L~ (Cage (C,n))))) `2 < (((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2 by A41, XREAL_1:226;
set p1 = |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]|;
A44: |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `1 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1 by EUCLID:52;
A45: |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `2 = (((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2 by EUCLID:52;
A46: ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 > ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 by A20, A25, A41, TOPREAL1:4;
then ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 <= (South-Bound (p,(L~ (Cage (C,n))))) `2 by A20, A25, TOPREAL1:4;
then ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 < |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `2 by A45, A43, XXREAL_0:2;
then A47: |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| in L~ (Cage (C,n)) by A1, A5, A39, A44, A45, A42, GOBOARD7:7, SPPOL_2:17;
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `2 <= ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2
proof
A48: ( ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 < ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 or ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 >= ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 ) ;
assume ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `2 > ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 ; :: thesis: contradiction
then ( (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2 in LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))))) or (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) in LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)) ) by A33, A39, A40, A46, A48, GOBOARD7:7;
then ( (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2 in {((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)} or (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) in {((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)} ) by A4, A10, A2, A25, A31, XBOOLE_0:def 4;
then ( (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1) = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1 or (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) ) by A33, TARSKI:def 1;
hence contradiction by A24, A22, A9, A7, A8, Th5; :: thesis: verum
end;
then A49: ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `2 <= (North-Bound (p,(L~ (Cage (C,n))))) `2 by A31, A36, TOPREAL1:4;
then |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `2 < (North-Bound (p,(L~ (Cage (C,n))))) `2 by A33, A45, A42, XXREAL_0:2;
then |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| in LSeg ((South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) by A26, A6, A38, A44, A45, A43, GOBOARD7:7;
then |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| in (LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) by A47, XBOOLE_0:def 4;
then |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((South-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| in {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A11, JORDAN18:22;
hence contradiction by A33, A45, A43, A42, A49, TARSKI:def 2; :: thesis: verum
end;
suppose A50: ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 < (North-Bound (p,(L~ (Cage (C,n))))) `2 ; :: thesis: contradiction
then A51: (((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2 < (North-Bound (p,(L~ (Cage (C,n))))) `2 by XREAL_1:226;
A52: ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 < (((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2 by A50, XREAL_1:226;
set p1 = |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]|;
A53: |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `1 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1 by EUCLID:52;
A54: |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `2 = (((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2 by EUCLID:52;
A55: ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 > ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `2 by A33, A31, A36, A50, TOPREAL1:4;
then (North-Bound (p,(L~ (Cage (C,n))))) `2 <= ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 by A31, A36, TOPREAL1:4;
then |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `2 < ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 by A54, A51, XXREAL_0:2;
then A56: |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| in L~ (Cage (C,n)) by A1, A33, A31, A40, A53, A54, A52, GOBOARD7:7, SPPOL_2:17;
((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 <= ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2
proof
A57: ( ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 < ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 or ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 >= ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 ) ;
assume ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1)) `2 > ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 ; :: thesis: contradiction
then ( (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2 in LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))))) or (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) in LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)) ) by A33, A39, A40, A55, A57, GOBOARD7:7;
then ( (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2 in {((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)} or (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) in {((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1)} ) by A4, A10, A2, A25, A31, XBOOLE_0:def 4;
then ( (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (1 + 1) = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1 or (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1) = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) ) by A33, TARSKI:def 1;
hence contradiction by A24, A22, A9, A7, A8, Th5; :: thesis: verum
end;
then A58: (South-Bound (p,(L~ (Cage (C,n))))) `2 <= ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 by A20, A25, TOPREAL1:4;
then (South-Bound (p,(L~ (Cage (C,n))))) `2 < |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| `2 by A54, A52, XXREAL_0:2;
then |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| in LSeg ((South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) by A26, A6, A38, A53, A54, A51, GOBOARD7:7;
then |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| in (LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) by A56, XBOOLE_0:def 4;
then |[(((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1),((((North-Bound (p,(L~ (Cage (C,n))))) `2) + (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2)) / 2)]| in {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A11, JORDAN18:22;
hence contradiction by A54, A52, A51, A58, TARSKI:def 2; :: thesis: verum
end;
end;
end;
suppose A59: ( LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) is vertical & LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) is horizontal ) ; :: thesis: contradiction
then A60: (North-Bound (p,(L~ (Cage (C,n))))) `2 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `2 by A31, A36, SPPOL_1:40;
(North-Bound (p,(L~ (Cage (C,n))))) `1 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))))) `1 by A26, A6, A13, A19, A33, A25, A59, JORDAN3:9, SPPOL_1:41;
then North-Bound (p,(L~ (Cage (C,n)))) = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) by A60, TOPREAL3:6;
then North-Bound (p,(L~ (Cage (C,n)))) in LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2)) by A33, RLTOPSP1:68;
then LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))) c= LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 2)) by A20, A25, TOPREAL1:6;
then p in L~ (Cage (C,n)) by A1, A30, A25, SPPOL_2:17;
then p in (LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) by A30, XBOOLE_0:def 4;
then p in {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A11, JORDAN18:22;
hence contradiction by A29, A28, TARSKI:def 2; :: thesis: verum
end;
suppose A61: ( LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) is horizontal & LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) is vertical ) ; :: thesis: contradiction
then A62: (South-Bound (p,(L~ (Cage (C,n))))) `2 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 by A13, A19, A25, JORDAN3:9, SPPOL_1:40;
(South-Bound (p,(L~ (Cage (C,n))))) `1 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `1 by A26, A6, A33, A31, A36, A61, SPPOL_1:41;
then South-Bound (p,(L~ (Cage (C,n)))) = (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1 by A62, TOPREAL3:6;
then South-Bound (p,(L~ (Cage (C,n)))) in LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))))) by A33, RLTOPSP1:68;
then LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))) c= LSeg (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))))) by A31, A36, TOPREAL1:6;
then p in L~ (Cage (C,n)) by A1, A30, A31, SPPOL_2:17;
then p in (LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) by A30, XBOOLE_0:def 4;
then p in {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A11, JORDAN18:22;
hence contradiction by A29, A28, TARSKI:def 2; :: thesis: verum
end;
suppose A63: ( LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),1) is horizontal & LSeg ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))),((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) is horizontal ) ; :: thesis: contradiction
then A64: (North-Bound (p,(L~ (Cage (C,n))))) `2 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)) `2 by A31, A36, SPPOL_1:40;
(South-Bound (p,(L~ (Cage (C,n))))) `2 = ((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) /. 1) `2 by A13, A19, A25, A63, JORDAN3:9, SPPOL_1:40;
hence contradiction by A29, A28, A3, A25, A31, A63, A64, SPRECT_3:9; :: thesis: verum
end;
end;
end;
North-Bound (p,(L~ (Cage (C,n)))) in L~ (Cage (C,n)) by A11, JORDAN18:17;
then A65: North-Bound (p,(L~ (Cage (C,n)))) in L~ rf by A1, A35, A32, XBOOLE_0:def 3;
len rf = (len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1 by FINSEQ_1:59, NAT_D:35;
then 1 + 1 <= len rf by A24, A23, NAT_1:13;
then A66: South-Bound (p,(L~ (Cage (C,n)))) in LSeg (rf,1) by A20, SPPOL_2:3;
A67: LSeg (rf,1) c= L~ rf by TOPREAL3:19;
then reconsider BCut = B_Cut (rf,(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) as S-Sequence_in_R2 by A11, A66, A65, JORDAN18:20, JORDAN3:37;
A68: (len BCut) + 1 >= 1 by NAT_1:11;
set Ga = GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>);
now :: thesis: for n being Nat st n in dom BCut holds
ex i, j being Nat st
( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & BCut /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) )
let n be Nat; :: thesis: ( n in dom BCut implies ex i, j being Nat st
( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & BCut /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) ) )
assume A69: n in dom BCut ; :: thesis: ex i, j being Nat st
( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & BCut /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) )
then A70: n <= len BCut by FINSEQ_3:25;
dom BCut c= dom (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) by Th23;
then consider i, j being Nat such that
A71: [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) and
A72: (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) by A69, GOBOARD2:14;
take i = i; :: thesis: ex j being Nat st
( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & BCut /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) )
take j = j; :: thesis: ( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & BCut /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) )
thus [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) by A71; :: thesis: BCut /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j)
1 <= n by A69, FINSEQ_3:25;
hence BCut /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) by A72, A70, FINSEQ_6:159; :: thesis: verum
end;
then consider BCut1 being FinSequence of (TOP-REAL 2) such that
A73: BCut1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) and
A74: BCut1 is being_S-Seq and
A75: L~ BCut = L~ BCut1 and
A76: BCut /. 1 = BCut1 /. 1 and
A77: BCut /. (len BCut) = BCut1 /. (len BCut1) and
A78: len BCut <= len BCut1 by GOBOARD3:2;
reconsider BCut1 = BCut1 as S-Sequence_in_R2 by A74;
A79: L~ BCut1 c= L~ rf by A67, A66, A65, A75, JORDAN5B:24;
A80: len BCut1 in dom BCut1 by FINSEQ_5:6;
A81: 1 in dom BCut1 by FINSEQ_5:6;
A82: now :: thesis: BCut1 is constant
assume BCut1 is constant ; :: thesis: contradiction
then BCut1 /. 1 = BCut1 /. (len BCut1) by A81, A80, FINSEQ_6:def 11;
then BCut1 /. (len BCut1) = South-Bound (p,(L~ (Cage (C,n)))) by A67, A66, A65, A76, Th19;
hence contradiction by A11, A67, A66, A65, A77, Th20, JORDAN18:20; :: thesis: verum
end;
BCut /. (len BCut) = North-Bound (p,(L~ (Cage (C,n)))) by A67, A66, A65, Th20;
then A83: North-Bound (p,(L~ (Cage (C,n)))) in LSeg ((BCut1 /. ((len BCut1) -' 1)),(BCut1 /. (len BCut1))) by A77, RLTOPSP1:68;
A84: len BCut1 >= 1 + 1 by TOPREAL1:def 8;
then A85: (len BCut1) - 1 >= 1 by XREAL_1:19;
take BCut ; :: thesis: ( BCut = B_Cut (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) & ex P being S-Sequence_in_R2 st
( P is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ P & P /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & P /. (len P) = South-Bound (p,(L~ (Cage (C,n)))) & len P >= 2 & ex B1 being S-Sequence_in_R2 st
( B1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ BCut = L~ B1 & BCut /. 1 = B1 /. 1 & BCut /. (len BCut) = B1 /. (len B1) & len BCut <= len B1 & ex g being constant standard special_circular_sequence st g = B1 ^' P ) ) )
thus BCut = B_Cut (((Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n))))))) | ((len (Rotate ((Cage (C,n)),((Cage (C,n)) /. (Index ((South-Bound (p,(L~ (Cage (C,n))))),(Cage (C,n)))))))) -' 1)),(South-Bound (p,(L~ (Cage (C,n))))),(North-Bound (p,(L~ (Cage (C,n)))))) ; :: thesis: ex P being S-Sequence_in_R2 st
( P is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ P & P /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & P /. (len P) = South-Bound (p,(L~ (Cage (C,n)))) & len P >= 2 & ex B1 being S-Sequence_in_R2 st
( B1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ BCut = L~ B1 & BCut /. 1 = B1 /. 1 & BCut /. (len BCut) = B1 /. (len B1) & len BCut <= len B1 & ex g being constant standard special_circular_sequence st g = B1 ^' P ) )
A86: (LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) = {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A11, JORDAN18:22;
len BCut > 0 by NAT_1:3;
then A87: len BCut >= 0 + 1 by NAT_1:13;
then A88: (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) /. (len BCut) = BCut /. (len BCut) by FINSEQ_6:159
.= North-Bound (p,(L~ (Cage (C,n)))) by A67, A66, A65, Th20
.= <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. 1 by FINSEQ_4:17 ;
A89: len <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = 1 + 1 by FINSEQ_1:44;
then A90: (len (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) + 1 = (len BCut) + (1 + 1) by FINSEQ_6:139
.= ((len BCut) + 1) + 1 ;
then A91: len BCut < len (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) by NAT_1:13;
now :: thesis: for n being Nat st n in dom <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> holds
ex i, j being Nat st
( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) )
let n be Nat; :: thesis: ( n in dom <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> implies ex i, j being Nat st
( [j,b3] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. i = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (j,b3) ) )
assume n in dom <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> ; :: thesis: ex i, j being Nat st
( [j,b3] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. i = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (j,b3) )
then A92: n in Seg 2 by FINSEQ_1:89;
per cases ( n = 1 or n = 1 + 1 ) by A92, FINSEQ_1:2, TARSKI:def 2;
suppose A93: n = 1 ; :: thesis: ex i, j being Nat st
( [j,b3] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. i = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (j,b3) )
len BCut in Seg (len (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) by A91, A87, FINSEQ_1:1;
then len BCut in dom (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) by FINSEQ_1:def 3;
then consider i, j being Nat such that
A94: [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) and
A95: (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) /. (len BCut) = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) by GOBOARD2:14;
take i = i; :: thesis: ex j being Nat st
( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) )
take j = j; :: thesis: ( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) )
thus [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) by A94; :: thesis: <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j)
thus <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) by A88, A93, A95; :: thesis: verum
end;
suppose A96: n = 1 + 1 ; :: thesis: ex i, j being Nat st
( [j,b3] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. i = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (j,b3) )
(len BCut) + 1 in dom (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) by A90, A68, FINSEQ_3:25;
then consider i, j being Nat such that
A97: [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) and
A98: (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) /. ((len BCut) + 1) = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) by GOBOARD2:14;
take i = i; :: thesis: ex j being Nat st
( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) )
take j = j; :: thesis: ( [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) & <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) )
thus [i,j] in Indices (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) by A97; :: thesis: <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j)
thus <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. n = (GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>)) * (i,j) by A89, A96, A98, FINSEQ_6:160; :: thesis: verum
end;
end;
end;
then consider pion1 being FinSequence of (TOP-REAL 2) such that
A99: pion1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) and
A100: pion1 is being_S-Seq and
A101: L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ pion1 and
A102: <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. 1 = pion1 /. 1 and
A103: <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> /. (len <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) = pion1 /. (len pion1) and
A104: len <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> <= len pion1 by A27, GOBOARD3:2;
reconsider pion1 = pion1 as S-Sequence_in_R2 by A100;
A105: pion1 /. (len pion1) = South-Bound (p,(L~ (Cage (C,n)))) by A89, A103, FINSEQ_4:17
.= BCut1 /. 1 by A67, A66, A65, A76, Th19 ;
A106: L~ rf c= L~ (Cage (C,n)) by A1, TOPREAL3:20;
then L~ BCut1 c= L~ (Cage (C,n)) by A79;
then (L~ BCut1) /\ (LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) c= {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A86, XBOOLE_1:26;
then (L~ BCut1) /\ (L~ pion1) c= {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A101, SPPOL_2:21;
then (L~ BCut1) /\ (L~ pion1) c= {(North-Bound (p,(L~ (Cage (C,n))))),(BCut1 /. 1)} by A67, A66, A65, A76, Th19;
then A107: (L~ BCut1) /\ (L~ pion1) c= {(BCut1 /. 1),(pion1 /. 1)} by A102, FINSEQ_4:17;
len BCut1 > 1 by A84, NAT_1:13;
then A108: ((len BCut1) -' 1) + 1 = len BCut1 by XREAL_1:235;
A109: BCut1 /. (len BCut1) = North-Bound (p,(L~ (Cage (C,n)))) by A67, A66, A65, A77, Th20
.= pion1 /. 1 by A102, FINSEQ_4:17 ;
then A110: BCut1 ^' pion1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) by A99, A73, TOPREAL8:12;
A111: L~ BCut1 c= L~ (Cage (C,n)) by A106, A79;
A112: now :: thesis: not South-Bound (p,(L~ (Cage (C,n)))) in LSeg (BCut1,((len BCut1) -' 1))
assume South-Bound (p,(L~ (Cage (C,n)))) in LSeg (BCut1,((len BCut1) -' 1)) ; :: thesis: contradiction
then South-Bound (p,(L~ (Cage (C,n)))) in LSeg ((BCut1 /. ((len BCut1) -' 1)),(BCut1 /. (len BCut1))) by A85, A108, TOPREAL1:def 3;
then LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))) c= LSeg ((BCut1 /. ((len BCut1) -' 1)),(BCut1 /. (len BCut1))) by A83, TOPREAL1:6;
then p in LSeg ((BCut1 /. ((len BCut1) -' 1)),(BCut1 /. (len BCut1))) by A30;
then p in LSeg (BCut1,((len BCut1) -' 1)) by A85, A108, TOPREAL1:def 3;
then p in L~ BCut1 by SPPOL_2:17;
then p in (LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) by A30, A111, XBOOLE_0:def 4;
then p in {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A11, JORDAN18:22;
hence contradiction by A29, A28, TARSKI:def 2; :: thesis: verum
end;
LSeg (BCut1,((len BCut1) -' 1)) c= L~ BCut1 by TOPREAL3:19;
then LSeg (BCut1,((len BCut1) -' 1)) c= L~ rf by A79;
then A113: LSeg (BCut1,((len BCut1) -' 1)) c= L~ (Cage (C,n)) by A106;
LSeg (pion1,1) c= L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> by A101, TOPREAL3:19;
then LSeg (pion1,1) c= LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))) by SPPOL_2:21;
then (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) c= (LSeg ((North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n))))))) /\ (L~ (Cage (C,n))) by A113, XBOOLE_1:27;
then A114: (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) c= {(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))} by A11, JORDAN18:22;
A115: (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) = {(BCut1 /. (len BCut1))}
proof
thus (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) c= {(BCut1 /. (len BCut1))} :: according to XBOOLE_0:def 10 :: thesis: {(BCut1 /. (len BCut1))} c= (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) or x in {(BCut1 /. (len BCut1))} )
assume A116: x in (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) ; :: thesis: x in {(BCut1 /. (len BCut1))}
then x <> South-Bound (p,(L~ (Cage (C,n)))) by A112, XBOOLE_0:def 4;
then x = North-Bound (p,(L~ (Cage (C,n)))) by A114, A116, TARSKI:def 2;
then x = BCut1 /. (len BCut1) by A67, A66, A65, A77, Th20;
hence x in {(BCut1 /. (len BCut1))} by TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(BCut1 /. (len BCut1))} or x in (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) )
assume x in {(BCut1 /. (len BCut1))} ; :: thesis: x in (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1))
then A117: x = BCut1 /. (len BCut1) by TARSKI:def 1;
then x in LSeg ((BCut1 /. ((len BCut1) -' 1)),(BCut1 /. (len BCut1))) by RLTOPSP1:68;
then A118: x in LSeg (BCut1,((len BCut1) -' 1)) by A85, A108, TOPREAL1:def 3;
x in LSeg ((pion1 /. 1),(pion1 /. (1 + 1))) by A109, A117, RLTOPSP1:68;
then x in LSeg (pion1,1) by A89, A104, TOPREAL1:def 3;
hence x in (LSeg (BCut1,((len BCut1) -' 1))) /\ (LSeg (pion1,1)) by A118, XBOOLE_0:def 4; :: thesis: verum
end;
take pion1 ; :: thesis: ( pion1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ pion1 & pion1 /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & pion1 /. (len pion1) = South-Bound (p,(L~ (Cage (C,n)))) & len pion1 >= 2 & ex B1 being S-Sequence_in_R2 st
( B1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ BCut = L~ B1 & BCut /. 1 = B1 /. 1 & BCut /. (len BCut) = B1 /. (len B1) & len BCut <= len B1 & ex g being constant standard special_circular_sequence st g = B1 ^' pion1 ) )
len <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = 2 by FINSEQ_1:44;
hence ( pion1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*> = L~ pion1 & pion1 /. 1 = North-Bound (p,(L~ (Cage (C,n)))) & pion1 /. (len pion1) = South-Bound (p,(L~ (Cage (C,n)))) & len pion1 >= 2 ) by A99, A101, A102, A103, A104, FINSEQ_4:17; :: thesis: ex B1 being S-Sequence_in_R2 st
( B1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ BCut = L~ B1 & BCut /. 1 = B1 /. 1 & BCut /. (len BCut) = B1 /. (len B1) & len BCut <= len B1 & ex g being constant standard special_circular_sequence st g = B1 ^' pion1 )
set g = BCut1 ^' pion1;
now :: thesis: not len BCut = 1
assume len BCut = 1 ; :: thesis: contradiction
then BCut /. 1 = North-Bound (p,(L~ (Cage (C,n)))) by A67, A66, A65, Th20;
hence contradiction by A12, A67, A66, A65, Th19; :: thesis: verum
end;
then len BCut > 1 by A87, XXREAL_0:1;
then len BCut1 > 1 by A78, XXREAL_0:2;
then A119: len BCut1 >= 1 + 1 by NAT_1:13;
{(BCut1 /. 1),(pion1 /. 1)} c= (L~ BCut1) /\ (L~ pion1)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(BCut1 /. 1),(pion1 /. 1)} or x in (L~ BCut1) /\ (L~ pion1) )
assume x in {(BCut1 /. 1),(pion1 /. 1)} ; :: thesis: x in (L~ BCut1) /\ (L~ pion1)
then A120: ( x = BCut1 /. 1 or x = pion1 /. 1 ) by TARSKI:def 2;
then A121: x in L~ BCut1 by A109, A119, JORDAN3:1;
x in L~ pion1 by A89, A104, A105, A120, JORDAN3:1;
hence x in (L~ BCut1) /\ (L~ pion1) by A121, XBOOLE_0:def 4; :: thesis: verum
end;
then (L~ BCut1) /\ (L~ pion1) = {(BCut1 /. 1),(pion1 /. 1)} by A107;
then reconsider g = BCut1 ^' pion1 as constant standard special_circular_sequence by A109, A82, A110, A115, A105, Th25, JORDAN8:4, TOPREAL8:11, TOPREAL8:33, TOPREAL8:34;
take BCut1 ; :: thesis: ( BCut1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ BCut = L~ BCut1 & BCut /. 1 = BCut1 /. 1 & BCut /. (len BCut) = BCut1 /. (len BCut1) & len BCut <= len BCut1 & ex g being constant standard special_circular_sequence st g = BCut1 ^' pion1 )
thus ( BCut1 is_sequence_on GoB (BCut ^' <*(North-Bound (p,(L~ (Cage (C,n))))),(South-Bound (p,(L~ (Cage (C,n)))))*>) & L~ BCut = L~ BCut1 & BCut /. 1 = BCut1 /. 1 & BCut /. (len BCut) = BCut1 /. (len BCut1) & len BCut <= len BCut1 ) by A73, A75, A76, A77, A78; :: thesis: ex g being constant standard special_circular_sequence st g = BCut1 ^' pion1
take g ; :: thesis: g = BCut1 ^' pion1
thus g = BCut1 ^' pion1 ; :: thesis: verum