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)))

proof

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;

now :: thesis: contradiction

per 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;

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;

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;

now :: thesis: contradiction

per 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;

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;

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;

end;

end;

hence contradiction ; :: thesis: verum

end;

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;

end;

end;

hence contradiction ; :: thesis: verum

end;

(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
.= (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)))

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

suppose x = W-min (L~ (Cage (C,n))) ; :: thesis: x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n)))

hence x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) by A31, A3, A32, A29, XBOOLE_0:def 4; :: thesis: verum

end;

suppose x = E-max (L~ (Cage (C,n))) ; :: thesis: x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n)))

hence x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) by A31, A3, A30, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;