let n be Element of 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 non 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 non 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 non 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:36, 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 by XBOOLE_0:def 7;
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:69;
len (Rotate (Cage C,n),((Cage C,n) /. (Index (South-Bound p,(L~ (Cage C,n))),(Cage C,n)))) >= 1 + 1 by GOBOARD7:36, 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 5;
A6: (South-Bound p,(L~ (Cage C,n))) `1 = p `1 by JORDAN18:20;
len (Cage C,n) > 4 by GOBOARD7:36;
then A7: ((len (Cage C,n)) -' 1) + 1 = len (Cage C,n) by XREAL_1:237, 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:36, 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:69;
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 non 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:25;
A13: South-Bound p,(L~ (Cage C,n)) in L~ (Cage C,n) by A11, JORDAN18:22;
then A14: Index (South-Bound p,(L~ (Cage C,n))),(Cage C,n) < len (Cage C,n) by JORDAN3:41;
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))

proof

let i be Nat; :: thesis: ( 1 <= i & i < Index (South-Bound p,(L~ (Cage C,n))),(Cage C,n) implies (Cage C,n) /. i <> (Cage C,n) /. (Index (South-Bound p,(L~ (Cage C,n))),(Cage C,n)) )
i in NAT by ORDINAL1:def 13;
hence ( 1 <= i & i < Index (South-Bound p,(L~ (Cage C,n))),(Cage C,n) implies (Cage C,n) /. i <> (Cage C,n) /. (Index (South-Bound p,(L~ (Cage C,n))),(Cage C,n)) ) by A14, GOBOARD7:38; :: thesis: verum

end;

1 <= Index (South-Bound p,(L~ (Cage C,n))),(Cage C,n) by A13, JORDAN3:41;
then A16: Index (South-Bound p,(L~ (Cage C,n))),(Cage C,n) in dom (Cage C,n) by A14, FINSEQ_3:27;
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:42;
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:22;
A18: (Cage C,n) /. (Index (South-Bound p,(L~ (Cage C,n))),(Cage C,n)) in rng (Cage C,n) by A16, PARTFUN2:4;
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:53;
then 1 < len ((Cage C,n) :- ((Cage C,n) /. (Index (South-Bound p,(L~ (Cage C,n))),(Cage C,n)))) by A17, XREAL_1:21;
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:234
.= LSeg (Cage C,n),(Index (South-Bound p,(L~ (Cage C,n))),(Cage C,n)) by A16, A15, FINSEQ_6:52 ;
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:42;
A21: len (Cage C,n) > 1 + 1 by GOBOARD7:36, XXREAL_0:2;
then A22: (len (Cage C,n)) - 1 > 1 by XREAL_1:22;
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 REVROT_1:14;
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 5;
A26: (North-Bound p,(L~ (Cage C,n))) `1 = p `1 by JORDAN18:20;
then LSeg (North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n))) is vertical by A6, SPPOL_1:37;
then A27: <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*> is being_S-Seq by A12, JORDAN1B:8;
A28: p `2 < (North-Bound p,(L~ (Cage C,n))) `2 by A11, JORDAN18:23;
A29: (South-Bound p,(L~ (Cage C,n))) `2 < p `2 by A11, JORDAN18:23;
then A30: p in LSeg (North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n))) by A26, A6, A28, GOBOARD7:8;
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 5;
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:49;
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:8;
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

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:41;

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:42, SPPOL_1:64;
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:37;
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:37;

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:228;
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:228;
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:56;
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:56;
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:10;
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:10;
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:8, 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:8;
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:10;
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:8;
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:27;
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:228;
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:228;
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:56;
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:56;
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:10;
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:10;
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:8, 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:8;
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:10;
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:8;
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:27;
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:63;
(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:42, SPPOL_1:64;
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:11;
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:69;
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:12;
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:27;
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:42, SPPOL_1:63;
(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:64;
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:11;
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:69;
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:12;
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:27;
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:63;
(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:42, SPPOL_1:63;
hence contradiction by A29, A28, A3, A25, A31, A63, A64, SPRECT_3:21; :: thesis: verum

end;

end;

end;

North-Bound p,(L~ (Cage C,n)) in L~ (Cage C,n) by A11, JORDAN18:22;
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:80, 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:26;
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:25, JORDAN3:72;
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

let n be Element of NAT ; :: thesis: ( n in dom BCut implies ex i, j being Element of 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 Element of 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:27;
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 Element of 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:25;
take i = i; :: thesis: ex j being Element of 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:27;
hence BCut /. n = (GoB (BCut ^' <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*>)) * i,j by A72, A70, GRAPH_2:61; :: 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:27;
A80: len BCut1 in dom BCut1 by FINSEQ_5:6;
A81: 1 in dom BCut1 by FINSEQ_5:6;

A82: now

assume BCut1 is constant ; :: thesis: contradiction
then BCut1 /. 1 = BCut1 /. (len BCut1) by A81, A80, REVROT_1:def 1;
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:25; :: 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:69;
A84: len BCut1 >= 1 + 1 by TOPREAL1:def 10;
then A85: (len BCut1) - 1 >= 1 by XREAL_1:21;
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 non 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 non 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:27;
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 GRAPH_2:61
.= 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:26 ;
A89: len <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*> = 1 + 1 by FINSEQ_1:61;
then A90: (len (BCut ^' <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*>)) + 1 = (len BCut) + (1 + 1) by GRAPH_2:13
.= ((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

let n be Element of NAT ; :: thesis: ( n in dom <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*> implies ex i, j being Element of NAT st
( [j,b₃] 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,b₃ ) )
assume n in dom <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*> ; :: thesis: ex i, j being Element of NAT st
( [j,b₃] 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,b₃ )
then A92: n in Seg 2 by FINSEQ_3:29;

per cases ( n = 1 or n = 1 + 1 ) by A92, FINSEQ_1:4, TARSKI:def 2;

suppose A93: n = 1 ; :: thesis: ex i, j being Element of NAT st
( [j,b₃] 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,b₃ )

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:3;
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 Element of 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:25;
take i = i; :: thesis: ex j being Element of 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 Element of NAT st
( [j,b₃] 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,b₃ )

(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:27;
then consider i, j being Element of 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:25;
take i = i; :: thesis: ex j being Element of 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, GRAPH_2:62; :: 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:26
.= BCut1 /. 1 by A67, A66, A65, A76, Th19 ;
A106: L~ rf c= L~ (Cage C,n) by A1, TOPREAL3:27;
then L~ BCut1 c= L~ (Cage C,n) by A79, XBOOLE_1:1;
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:26;
len BCut1 > 1 by A84, NAT_1:13;
then A108: ((len BCut1) -' 1) + 1 = len BCut1 by XREAL_1:237;
A109: BCut1 /. (len BCut1) = North-Bound p,(L~ (Cage C,n)) by A67, A66, A65, A77, Th20
.= pion1 /. 1 by A102, FINSEQ_4:26 ;
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, XBOOLE_1:1;

A112: now

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 5;
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:12;
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 5;
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:27;
hence contradiction by A29, A28, TARSKI:def 2; :: thesis: verum

end;

LSeg BCut1,((len BCut1) -' 1) c= L~ BCut1 by TOPREAL3:26;
then LSeg BCut1,((len BCut1) -' 1) c= L~ rf by A79, XBOOLE_1:1;
then A113: LSeg BCut1,((len BCut1) -' 1) c= L~ (Cage C,n) by A106, XBOOLE_1:1;
LSeg pion1,1 c= L~ <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*> by A101, TOPREAL3:26;
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:27;
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 set ; :: 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 set ; :: 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:69;
then A118: x in LSeg BCut1,((len BCut1) -' 1) by A85, A108, TOPREAL1:def 5;
x in LSeg (pion1 /. 1),(pion1 /. (1 + 1)) by A109, A117, RLTOPSP1:69;
then x in LSeg pion1,1 by A89, A104, TOPREAL1:def 5;
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 non 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:61;
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:26; :: 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 non constant standard special_circular_sequence st g = B1 ^' pion1 )
set g = BCut1 ^' pion1;

now

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 set ; :: 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:34;
x in L~ pion1 by A89, A104, A105, A120, JORDAN3:34;
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, XBOOLE_0:def 10;
then reconsider g = BCut1 ^' pion1 as non constant standard special_circular_sequence by A109, A82, A110, A115, A105, Th25, JORDAN8:7, 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 non 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 non constant standard special_circular_sequence st g = BCut1 ^' pion1
take g ; :: thesis: g = BCut1 ^' pion1
thus g = BCut1 ^' pion1 ; :: thesis: verum