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));
assume A1:
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 ) ) )
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);
A2:
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;
A3:
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;
A4:
len (Cage C,n) > 4
by GOBOARD7:36;
A5:
len (Cage C,n) > 1 + 1
by GOBOARD7:36, XXREAL_0:2;
then A6:
(len (Cage C,n)) - 1 > 1
by XREAL_1:22;
then A7:
1 < (len (Cage C,n)) -' 1
by XREAL_0:def 2;
A8:
len (Cage C,n) > 1
by GOBOARD7:36, XXREAL_0:2;
A9:
((len (Cage C,n)) -' 1) + 1 = len (Cage C,n)
by A4, XREAL_1:237, XXREAL_0:2;
then 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 A3, A6, JORDAN4:49;
A10:
North-Bound p,(L~ (Cage C,n)) <> South-Bound p,(L~ (Cage C,n))
by A1, JORDAN18:25;
A11:
( (North-Bound p,(L~ (Cage C,n))) `1 = p `1 & (South-Bound p,(L~ (Cage C,n))) `1 = p `1 )
by JORDAN18:20;
A12:
( (South-Bound p,(L~ (Cage C,n))) `2 < p `2 & p `2 < (North-Bound p,(L~ (Cage C,n))) `2 )
by A1, JORDAN18:23;
then A13:
p in LSeg (North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))
by A11, GOBOARD7:8;
A14:
L~ rf c= L~ (Cage C,n)
by A2, TOPREAL3:27;
A15:
( North-Bound p,(L~ (Cage C,n)) in L~ (Cage C,n) & South-Bound p,(L~ (Cage C,n)) in L~ (Cage C,n) )
by A1, JORDAN18:22;
then A16:
( 1 <= Index (South-Bound p,(L~ (Cage C,n))),(Cage C,n) & Index (South-Bound p,(L~ (Cage C,n))),(Cage C,n) < len (Cage C,n) )
by JORDAN3:41;
then A17:
Index (South-Bound p,(L~ (Cage C,n))),(Cage C,n) in dom (Cage C,n)
by FINSEQ_3:27;
then A18:
(Cage C,n) /. (Index (South-Bound p,(L~ (Cage C,n))),(Cage C,n)) in rng (Cage C,n)
by PARTFUN2:4;
A19:
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 A16, GOBOARD7:38;
:: thesis: verum
end;
A20:
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 A18, FINSEQ_5:53;
((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 A17, 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 A16, XXREAL_0:2;
then
(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;
then
1 < len ((Cage C,n) :- ((Cage C,n) /. (Index (South-Bound p,(L~ (Cage C,n))),(Cage C,n))))
by A20, XREAL_1:21;
then A21: 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 A17, A19, FINSEQ_6:52
;
then A22:
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 A15, JORDAN3:42;
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 A23:
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;
A24:
LSeg (North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n))) is vertical
by A11, SPPOL_1:37;
A25:
(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;
A26:
( (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) & (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;
A27:
(len (Cage C,n)) -' 1 < len (Cage C,n)
by A9, NAT_1:13;
A28:
(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 A29:
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;
A30:
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 A3, A5, TOPREAL1:def 5;
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 A3, A6, A9, TOPREAL1:def 5;
A32:
(South-Bound p,(L~ (Cage C,n))) `2 < (North-Bound p,(L~ (Cage C,n))) `2
by A12, XXREAL_0:2;
A33:
now assume A34:
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: contradictionper 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 A35:
(
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: contradictionthen A36:
(
((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 &
((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 A30, A31, SPPOL_1:37;
A37:
(
(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)) `1 &
(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 A15, A21, A30, A31, A34, A35, JORDAN3:42, SPPOL_1:64;
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 A32, XXREAL_0:2;
suppose A38:
(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: contradictionset 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)]|;
A39:
(
|[(((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 &
|[(((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;
A40:
(
(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 &
(((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 A38, XREAL_1:228;
A41:
((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 A22, A30, A38, 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 A22, A30, 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 A39, A40, XXREAL_0:2;
then A42:
|[(((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 A2, A23, A36, A39, A40, 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
assume A43:
((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
(
((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 )
;
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 A25, A36, A41, A43, 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 A26, A28, A30, 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 A25, TARSKI:def 1;
hence
contradiction
by A3, A6, A8, A9, A27, Th5;
:: thesis: verum
end; then A44:
((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, A34, 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 A25, A39, A40, 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 A11, A37, A39, A40, 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 A42, 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 A1, JORDAN18:27;
hence
contradiction
by A25, A39, A40, A44, TARSKI:def 2;
:: thesis: verum end; suppose A45:
((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: contradictionset 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)]|;
A46:
(
|[(((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 &
|[(((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;
A47:
(
((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 &
(((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 A45, XREAL_1:228;
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)))) /. (len (Rotate (Cage C,n),((Cage C,n) /. (Index (South-Bound p,(L~ (Cage C,n))),(Cage C,n)))))) `2
by A25, A31, A34, A45, 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, A34, 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 A46, A47, XXREAL_0:2;
then A49:
|[(((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 A2, A25, A31, A36, A46, A47, 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
assume A50:
((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
(
((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 )
;
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 A25, A36, A48, A50, 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 A26, A28, A30, 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 A25, TARSKI:def 1;
hence
contradiction
by A3, A6, A8, A9, A27, Th5;
:: thesis: verum
end; then A51:
(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 A22, A30, 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 A46, A47, 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 A11, A37, A46, A47, 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 A49, 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 A1, JORDAN18:27;
hence
contradiction
by A46, A47, A51, TARSKI:def 2;
:: thesis: verum end; end; suppose A52:
(
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: contradictionthen A53:
(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 A11, A15, A21, A25, A30, JORDAN3:42, SPPOL_1:64;
(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, A34, A52, SPPOL_1:63;
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 A53, 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 A25, 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 A22, A30, TOPREAL1:12;
then
p in L~ (Cage C,n)
by A2, A13, A30, 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 A13, XBOOLE_0:def 4;
then
p in {(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))}
by A1, JORDAN18:27;
hence
contradiction
by A12, TARSKI:def 2;
:: thesis: verum end; suppose A54:
(
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: contradictionthen A55:
(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 A11, A25, A31, A34, SPPOL_1:64;
(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 A15, A21, A30, A54, JORDAN3:42, SPPOL_1:63;
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 A55, 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 A25, 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, A34, TOPREAL1:12;
then
p in L~ (Cage C,n)
by A2, A13, 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 A13, XBOOLE_0:def 4;
then
p in {(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))}
by A1, JORDAN18:27;
hence
contradiction
by A12, TARSKI:def 2;
:: thesis: verum end; suppose A56:
(
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: contradictionthen
(
(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 &
(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 A15, A21, A30, A31, A34, JORDAN3:42, SPPOL_1:63;
hence
contradiction
by A12, A29, A30, A31, A56, SPRECT_3:21;
:: thesis: verum end; end;
A57:
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 A3, A6, A9, GOBOARD2:8;
A58:
LSeg rf,1 c= L~ rf
by TOPREAL3:26;
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 A3, A7, NAT_1:13;
then
South-Bound p,(L~ (Cage C,n)) in LSeg rf,1
by A22, SPPOL_2:3;
then A59:
( North-Bound p,(L~ (Cage C,n)) in L~ rf & South-Bound p,(L~ (Cage C,n)) in L~ rf )
by A2, A15, A33, A57, A58, XBOOLE_0:def 3;
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 A1, JORDAN18:25, JORDAN3:72;
set pion = <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*>;
set Ga = GoB (BCut ^' <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*>);
A60:
len <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*> = 1 + 1
by FINSEQ_1:61;
then A61: (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 A62:
len BCut < len (BCut ^' <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*>)
by NAT_1:13;
A63:
(len BCut) + 1 >= 1
by NAT_1:11;
len BCut > 0
by NAT_1:3;
then A64:
len BCut >= 0 + 1
by NAT_1:13;
then A65: (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 A59, Th20
.=
<*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*> /. 1
by FINSEQ_4:26
;
A66:
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,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 Element of 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 A67:
n in Seg 2
by FINSEQ_3:29;
per cases
( n = 1 or n = 1 + 1 )
by A67, FINSEQ_1:4, TARSKI:def 2;
suppose A68:
n = 1
;
:: thesis: ex i, j being Element of 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 A62, A64, 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 A69:
[i,j] in Indices (GoB (BCut ^' <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*>))
and A70:
(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 A69;
:: 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,jthus
<*(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 A65, A68, A70;
:: thesis: verum end; suppose A71:
n = 1
+ 1
;
:: thesis: ex i, j being Element of 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 A61, A63, FINSEQ_3:27;
then consider i,
j being
Element of
NAT such that A72:
[i,j] in Indices (GoB (BCut ^' <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*>))
and A73:
(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 A72;
:: 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,jthus
<*(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 A60, A71, A73, GRAPH_2:62;
:: thesis: verum end; end;
<*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*> is being_S-Seq
by A10, A24, JORDAN1B:8;
then consider pion1 being FinSequence of (TOP-REAL 2) such that
A74:
pion1 is_sequence_on GoB (BCut ^' <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*>)
and
A75:
pion1 is being_S-Seq
and
A76:
L~ <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*> = L~ pion1
and
A77:
<*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*> /. 1 = pion1 /. 1
and
A78:
<*(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
A79:
len <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*> <= len pion1
by A66, GOBOARD3:2;
reconsider pion1 = pion1 as S-Sequence_in_R2 by A75;
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 A80:
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 )
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 A81:
[i,j] in Indices (GoB (BCut ^' <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*>))
and A82:
(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 A80, 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 A81;
:: thesis: BCut /. n = (GoB (BCut ^' <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*>)) * i,j
( 1
<= n &
n <= len BCut )
by A80, 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 A82, GRAPH_2:61;
:: thesis: verum end;
then consider BCut1 being FinSequence of (TOP-REAL 2) such that
A83:
BCut1 is_sequence_on GoB (BCut ^' <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*>)
and
A84:
BCut1 is being_S-Seq
and
A85:
L~ BCut = L~ BCut1
and
A86:
BCut /. 1 = BCut1 /. 1
and
A87:
BCut /. (len BCut) = BCut1 /. (len BCut1)
and
A88:
len BCut <= len BCut1
by GOBOARD3:2;
reconsider BCut1 = BCut1 as S-Sequence_in_R2 by A84;
set g = BCut1 ^' pion1;
A89: BCut1 /. (len BCut1) =
North-Bound p,(L~ (Cage C,n))
by A59, A87, Th20
.=
pion1 /. 1
by A77, FINSEQ_4:26
;
A90:
( 1 in dom BCut1 & len BCut1 in dom BCut1 )
by FINSEQ_5:6;
A92:
BCut1 ^' pion1 is_sequence_on GoB (BCut ^' <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*>)
by A74, A83, A89, TOPREAL8:12;
A93:
L~ BCut1 c= L~ rf
by A59, A85, JORDAN5B:27;
LSeg BCut1,((len BCut1) -' 1) c= L~ BCut1
by TOPREAL3:26;
then
LSeg BCut1,((len BCut1) -' 1) c= L~ rf
by A93, XBOOLE_1:1;
then A94:
LSeg BCut1,((len BCut1) -' 1) c= L~ (Cage C,n)
by A14, XBOOLE_1:1;
LSeg pion1,1 c= L~ <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*>
by A76, 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 A94, XBOOLE_1:27;
then A95:
(LSeg BCut1,((len BCut1) -' 1)) /\ (LSeg pion1,1) c= {(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))}
by A1, JORDAN18:27;
A96:
len BCut1 >= 1 + 1
by TOPREAL1:def 10;
then A97:
(len BCut1) - 1 >= 1
by XREAL_1:21;
len BCut1 > 1
by A96, NAT_1:13;
then A98:
((len BCut1) -' 1) + 1 = len BCut1
by XREAL_1:237;
BCut /. (len BCut) = North-Bound p,(L~ (Cage C,n))
by A59, Th20;
then A99:
North-Bound p,(L~ (Cage C,n)) in LSeg (BCut1 /. ((len BCut1) -' 1)),(BCut1 /. (len BCut1))
by A87, RLTOPSP1:69;
A100:
L~ BCut1 c= L~ (Cage C,n)
by A14, A93, XBOOLE_1:1;
A101:
now assume
South-Bound p,
(L~ (Cage C,n)) in LSeg BCut1,
((len BCut1) -' 1)
;
:: thesis: contradictionthen
South-Bound p,
(L~ (Cage C,n)) in LSeg (BCut1 /. ((len BCut1) -' 1)),
(BCut1 /. (len BCut1))
by A97, A98, 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 A99, TOPREAL1:12;
then
p in LSeg (BCut1 /. ((len BCut1) -' 1)),
(BCut1 /. (len BCut1))
by A13;
then
p in LSeg BCut1,
((len BCut1) -' 1)
by A97, A98, 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 A13, A100, XBOOLE_0:def 4;
then
p in {(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))}
by A1, JORDAN18:27;
hence
contradiction
by A12, TARSKI:def 2;
:: thesis: verum end;
A102:
(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 A103:
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 A101, XBOOLE_0:def 4;
then
x = North-Bound p,
(L~ (Cage C,n))
by A95, A103, TARSKI:def 2;
then
x = BCut1 /. (len BCut1)
by A59, A87, 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 A104:
x = BCut1 /. (len BCut1)
by TARSKI:def 1;
then
x in LSeg (BCut1 /. ((len BCut1) -' 1)),
(BCut1 /. (len BCut1))
by RLTOPSP1:69;
then A105:
x in LSeg BCut1,
((len BCut1) -' 1)
by A97, A98, TOPREAL1:def 5;
x in LSeg (pion1 /. 1),
(pion1 /. (1 + 1))
by A89, A104, RLTOPSP1:69;
then
x in LSeg pion1,1
by A60, A79, TOPREAL1:def 5;
hence
x in (LSeg BCut1,((len BCut1) -' 1)) /\ (LSeg pion1,1)
by A105, XBOOLE_0:def 4;
:: thesis: verum
end;
A106: pion1 /. (len pion1) =
South-Bound p,(L~ (Cage C,n))
by A60, A78, FINSEQ_4:26
.=
BCut1 /. 1
by A59, A86, Th19
;
then
len BCut > 1
by A64, XXREAL_0:1;
then
len BCut1 > 1
by A88, XXREAL_0:2;
then A107:
len BCut1 >= 1 + 1
by NAT_1:13;
A108:
(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 A1, JORDAN18:27;
L~ BCut1 c= L~ (Cage C,n)
by A14, A93, 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 A108, XBOOLE_1:26;
then
(L~ BCut1) /\ (L~ pion1) c= {(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))}
by A76, SPPOL_2:21;
then
(L~ BCut1) /\ (L~ pion1) c= {(North-Bound p,(L~ (Cage C,n))),(BCut1 /. 1)}
by A59, A86, Th19;
then A109:
(L~ BCut1) /\ (L~ pion1) c= {(BCut1 /. 1),(pion1 /. 1)}
by A77, FINSEQ_4:26;
{(BCut1 /. 1),(pion1 /. 1)} c= (L~ BCut1) /\ (L~ pion1)
then
(L~ BCut1) /\ (L~ pion1) = {(BCut1 /. 1),(pion1 /. 1)}
by A109, XBOOLE_0:def 10;
then reconsider g = BCut1 ^' pion1 as non constant standard special_circular_sequence by A89, A91, A92, A102, A106, Th25, JORDAN8:7, TOPREAL8:11, TOPREAL8:33, TOPREAL8:34;
A110:
len <*(North-Bound p,(L~ (Cage C,n))),(South-Bound p,(L~ (Cage C,n)))*> = 2
by FINSEQ_1:61;
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 ) )
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 ) )
thus
( 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 A74, A76, A77, A78, A79, A110, 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 )
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 A83, A85, A86, A87, A88; :: 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