let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Nat holds (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) = {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}

let n be Nat; :: thesis: (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) = {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}

E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;

then A1: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;

A2: len (Upper_Seq (C,n)) >= 3 by Th15;

then A3: rng (Upper_Seq (C,n)) c= L~ (Upper_Seq (C,n)) by SPPOL_2:18, XXREAL_0:2;

A4: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;

thus (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) c= {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} :: according to XBOOLE_0:def 10 :: thesis: {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n)))

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by FINSEQ_6:def 1

.= W-min (L~ (Cage (C,n))) by A4, FINSEQ_6:92 ;

then A29: W-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) by FINSEQ_6:168;

(E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ;

then A30: ( E-max (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & E-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) ) by A1, FINSEQ_5:46, FINSEQ_6:61;

len (Lower_Seq (C,n)) >= 3 by Th15;

then A31: rng (Lower_Seq (C,n)) c= L~ (Lower_Seq (C,n)) by SPPOL_2:18, XXREAL_0:2;

(Upper_Seq (C,n)) /. 1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by A1, FINSEQ_5:44

.= W-min (L~ (Cage (C,n))) by A4, FINSEQ_6:92 ;

then A32: W-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) by FINSEQ_6:42;

thus {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) :: thesis: verum

let n be Nat; :: thesis: (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) = {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}

E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;

then A1: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;

A2: len (Upper_Seq (C,n)) >= 3 by Th15;

then A3: rng (Upper_Seq (C,n)) c= L~ (Upper_Seq (C,n)) by SPPOL_2:18, XXREAL_0:2;

A4: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;

thus (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) c= {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} :: according to XBOOLE_0:def 10 :: thesis: {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n)))

proof

(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) =
(Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))
by A1, FINSEQ_5:54
set pW = W-min (L~ (Cage (C,n)));

set pE = E-max (L~ (Cage (C,n)));

set f = Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))));

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) or x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} )

assume A5: x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) ; :: thesis: x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}

then reconsider x1 = x as Point of (TOP-REAL 2) ;

assume A6: not x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} ; :: thesis: contradiction

x in L~ (Upper_Seq (C,n)) by A5, XBOOLE_0:def 4;

then consider i1 being Nat such that

A7: 1 <= i1 and

A8: i1 + 1 <= len (Upper_Seq (C,n)) and

A9: x1 in LSeg ((Upper_Seq (C,n)),i1) by SPPOL_2:13;

A10: LSeg ((Upper_Seq (C,n)),i1) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1) by A8, SPPOL_2:9;

x in L~ (Lower_Seq (C,n)) by A5, XBOOLE_0:def 4;

then consider i2 being Nat such that

A11: 1 <= i2 and

A12: i2 + 1 <= len (Lower_Seq (C,n)) and

A13: x1 in LSeg ((Lower_Seq (C,n)),i2) by SPPOL_2:13;

set i3 = i2 -' 1;

A14: (i2 -' 1) + 1 = i2 by A11, XREAL_1:235;

then A15: 1 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <= ((i2 -' 1) + 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A11, XREAL_1:7;

A16: len (Lower_Seq (C,n)) = ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by Th9;

then i2 < ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by A12, NAT_1:13;

then i2 - 1 < (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:19;

then A17: (i2 - 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by XREAL_1:20;

i2 - 1 >= 1 - 1 by A11, XREAL_1:9;

then A18: (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A17, XREAL_0:def 2;

A19: LSeg ((Lower_Seq (C,n)),i2) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))))) by A1, A14, SPPOL_2:10;

A20: len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by Th8;

then i1 + 1 < ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + 1 by A8, NAT_1:13;

then i1 + 1 < ((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by A15, XXREAL_0:2;

then A21: i1 + 1 <= (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by NAT_1:13;

A22: (((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) -' 1) + 1 = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A1, FINSEQ_4:21, XREAL_1:235;

(i2 -' 1) + 1 < ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by A12, A14, A16, NAT_1:13;

then i2 -' 1 < (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:7;

then A23: (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by XREAL_1:20;

then A24: ((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by NAT_1:13;

end;set pE = E-max (L~ (Cage (C,n)));

set f = Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))));

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) or x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} )

assume A5: x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) ; :: thesis: x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}

then reconsider x1 = x as Point of (TOP-REAL 2) ;

assume A6: not x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} ; :: thesis: contradiction

x in L~ (Upper_Seq (C,n)) by A5, XBOOLE_0:def 4;

then consider i1 being Nat such that

A7: 1 <= i1 and

A8: i1 + 1 <= len (Upper_Seq (C,n)) and

A9: x1 in LSeg ((Upper_Seq (C,n)),i1) by SPPOL_2:13;

A10: LSeg ((Upper_Seq (C,n)),i1) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1) by A8, SPPOL_2:9;

x in L~ (Lower_Seq (C,n)) by A5, XBOOLE_0:def 4;

then consider i2 being Nat such that

A11: 1 <= i2 and

A12: i2 + 1 <= len (Lower_Seq (C,n)) and

A13: x1 in LSeg ((Lower_Seq (C,n)),i2) by SPPOL_2:13;

set i3 = i2 -' 1;

A14: (i2 -' 1) + 1 = i2 by A11, XREAL_1:235;

then A15: 1 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <= ((i2 -' 1) + 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A11, XREAL_1:7;

A16: len (Lower_Seq (C,n)) = ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by Th9;

then i2 < ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by A12, NAT_1:13;

then i2 - 1 < (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:19;

then A17: (i2 - 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by XREAL_1:20;

i2 - 1 >= 1 - 1 by A11, XREAL_1:9;

then A18: (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A17, XREAL_0:def 2;

A19: LSeg ((Lower_Seq (C,n)),i2) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))))) by A1, A14, SPPOL_2:10;

A20: len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by Th8;

then i1 + 1 < ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + 1 by A8, NAT_1:13;

then i1 + 1 < ((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by A15, XXREAL_0:2;

then A21: i1 + 1 <= (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by NAT_1:13;

A22: (((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) -' 1) + 1 = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A1, FINSEQ_4:21, XREAL_1:235;

(i2 -' 1) + 1 < ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by A12, A14, A16, NAT_1:13;

then i2 -' 1 < (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:7;

then A23: (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by XREAL_1:20;

then A24: ((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by NAT_1:13;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( ( i1 + 1 < (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) & i1 > 1 ) or i1 = 1 or i1 + 1 = (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) )
by A7, A21, XXREAL_0:1;

end;

suppose
( i1 + 1 < (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) & i1 > 1 )
; :: thesis: contradiction

then
LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1) misses LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))))
by A23, GOBOARD5:def 4;

then (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1)) /\ (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))))) = {} ;

hence contradiction by A9, A13, A10, A19, XBOOLE_0:def 4; :: thesis: verum

end;then (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1)) /\ (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))))) = {} ;

hence contradiction by A9, A13, A10, A19, XBOOLE_0:def 4; :: thesis: verum

suppose A25:
i1 = 1
; :: thesis: contradiction

(i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) >= 0 + 3
by A2, A20, XREAL_1:7;

then A26: i1 + 1 < (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A25, XXREAL_0:2;

end;then A26: i1 + 1 < (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A25, XXREAL_0:2;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( ((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) or ((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 = len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) )
by A24, XXREAL_0:1;

end;

suppose
((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
; :: thesis: contradiction

then
LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1) misses LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))))
by A26, GOBOARD5:def 4;

then (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1)) /\ (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))))) = {} ;

hence contradiction by A9, A13, A10, A19, XBOOLE_0:def 4; :: thesis: verum

end;then (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1)) /\ (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))))) = {} ;

hence contradiction by A9, A13, A10, A19, XBOOLE_0:def 4; :: thesis: verum

suppose
((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 = len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
; :: thesis: contradiction

then
(i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) = (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - 1
;

then (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) = (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) -' 1 by XREAL_0:def 2;

then (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1)) /\ (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))))) = {((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1)} by A25, GOBOARD7:34, REVROT_1:30;

then x1 in {((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1)} by A9, A13, A10, A19, XBOOLE_0:def 4;

then x1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by TARSKI:def 1

.= W-min (L~ (Cage (C,n))) by A4, FINSEQ_6:92 ;

hence contradiction by A6, TARSKI:def 2; :: thesis: verum

end;then (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) = (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) -' 1 by XREAL_0:def 2;

then (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1)) /\ (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))))) = {((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1)} by A25, GOBOARD7:34, REVROT_1:30;

then x1 in {((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1)} by A9, A13, A10, A19, XBOOLE_0:def 4;

then x1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by TARSKI:def 1

.= W-min (L~ (Cage (C,n))) by A4, FINSEQ_6:92 ;

hence contradiction by A6, TARSKI:def 2; :: thesis: verum

suppose A27:
i1 + 1 = (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))
; :: thesis: contradiction

(i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) >= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
by NAT_1:11;

then (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A18, XXREAL_0:2;

then ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by NAT_1:13;

then A28: (((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) -' 1) + (1 + 1) <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A22;

0 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <= (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:7;

then (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = i1 + 1 by A8, A20, A27, XXREAL_0:1;

then (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1)) /\ (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))))) = {((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))))} by A7, A22, A27, A28, TOPREAL1:def 6;

then x1 in {((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))))} by A9, A13, A10, A19, XBOOLE_0:def 4;

then x1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by TARSKI:def 1

.= E-max (L~ (Cage (C,n))) by A1, FINSEQ_5:38 ;

hence contradiction by A6, TARSKI:def 2; :: thesis: verum

end;then (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A18, XXREAL_0:2;

then ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by NAT_1:13;

then A28: (((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) -' 1) + (1 + 1) <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A22;

0 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <= (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:7;

then (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = i1 + 1 by A8, A20, A27, XXREAL_0:1;

then (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1)) /\ (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))))) = {((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))))} by A7, A22, A27, A28, TOPREAL1:def 6;

then x1 in {((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))))} by A9, A13, A10, A19, XBOOLE_0:def 4;

then x1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by TARSKI:def 1

.= E-max (L~ (Cage (C,n))) by A1, FINSEQ_5:38 ;

hence contradiction by A6, TARSKI:def 2; :: thesis: verum

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by FINSEQ_6:def 1

.= W-min (L~ (Cage (C,n))) by A4, FINSEQ_6:92 ;

then A29: W-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) by FINSEQ_6:168;

(E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ;

then A30: ( E-max (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & E-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) ) by A1, FINSEQ_5:46, FINSEQ_6:61;

len (Lower_Seq (C,n)) >= 3 by Th15;

then A31: rng (Lower_Seq (C,n)) c= L~ (Lower_Seq (C,n)) by SPPOL_2:18, XXREAL_0:2;

(Upper_Seq (C,n)) /. 1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by A1, FINSEQ_5:44

.= W-min (L~ (Cage (C,n))) by A4, FINSEQ_6:92 ;

then A32: W-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) by FINSEQ_6:42;

thus {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} or x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) )

assume A33: x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} ; :: thesis: x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n)))

end;assume A33: x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} ; :: thesis: x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n)))

per cases
( x = W-min (L~ (Cage (C,n))) or x = E-max (L~ (Cage (C,n))) )
by A33, TARSKI:def 2;

end;