let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Element of 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 Element of 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:50;
then A1: E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by FINSEQ_6:96, SPRECT_2:47;
A2: len (Upper_Seq C,n) >= 3 by Th19;
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:47;
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 set ; :: 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 Element of 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 Element of 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:237;
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:9;
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 Th13;
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:21;
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:22;
i2 - 1 >= 1 - 1 by A11, XREAL_1:11;
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: (i2 -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) >= 0 by NAT_1:2;
A20: 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;
A21: len (Upper_Seq C,n) = (E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by Th12;
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 A22: i1 + 1 <= (i2 -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) by NAT_1:13;
A23: (((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:31, XREAL_1:237;
(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:9;
then A24: (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:22;
then A25: ((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

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, A22, 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 A24, 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))))))) = {} by XBOOLE_0:def 7;
hence contradiction by A9, A13, A10, A20, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A26: 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, A21, XREAL_1:9;
then A27: i1 + 1 < (i2 -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) by A26, XXREAL_0:2;

now

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 A25, 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 A27, 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))))))) = {} by XBOOLE_0:def 7;
hence contradiction by A9, A13, A10, A20, 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 A19, 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 A26, GOBOARD7:36, REVROT_1:30;
then x1 in {((Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1)} by A9, A13, A10, A20, 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:98 ;
hence contradiction by A6, TARSKI:def 2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A28: 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 A29: (((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 A23;
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:9;
then (E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) = i1 + 1 by A8, A21, A28, 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, A23, A28, A29, TOPREAL1:def 8;
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, A20, 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:41 ;
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:57
.= (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:98 ;
then A30: W-min (L~ (Cage C,n)) in rng (Lower_Seq C,n) by REVROT_1:3;
(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 A31: ( 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:49, FINSEQ_6:66;
len (Lower_Seq C,n) >= 3 by Th19;
then A32: 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:47
.= W-min (L~ (Cage C,n)) by A4, FINSEQ_6:98 ;
then A33: W-min (L~ (Cage C,n)) in rng (Upper_Seq C,n) by FINSEQ_6:46;
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 set ; :: 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 A34: 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 A34, 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 A32, A3, A33, A30, 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 A32, A3, A31, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;