let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT holds
( len (Upper_Seq C,n) >= 3 & len (Lower_Seq C,n) >= 3 )
let n be Element of NAT ; :: thesis: ( len (Upper_Seq C,n) >= 3 & len (Lower_Seq C,n) >= 3 )
set pWi = W-min (L~ (Cage C,n));
set pWa = W-max (L~ (Cage C,n));
set pEi = E-min (L~ (Cage C,n));
set pEa = E-max (L~ (Cage C,n));
A1: W-min (L~ (Cage C,n)) <> E-max (L~ (Cage C,n)) by TOPREAL5:25;
set f = Rotate (Cage C,n),(W-min (L~ (Cage C,n)));
A2: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A3: 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;
then (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 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 A2, FINSEQ_6:98 ;
then A4: ( E-max (L~ (Cage C,n)) in rng (Lower_Seq C,n) & W-min (L~ (Cage C,n)) in rng (Lower_Seq C,n) ) by FINSEQ_6:66, 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 A5: E-max (L~ (Cage C,n)) in rng (Upper_Seq C,n) by A3, FINSEQ_5:49;
W-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:48;
then A6: W-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by FINSEQ_6:96, SPRECT_2:47;
A7: (Upper_Seq C,n) /. 1 = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1 by A3, FINSEQ_5:47;
then A8: (Upper_Seq C,n) /. 1 = W-min (L~ (Cage C,n)) by A2, FINSEQ_6:98;
then A9: W-min (L~ (Cage C,n)) in rng (Upper_Seq C,n) by FINSEQ_6:46;
A10: L~ (Cage C,n) = L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by REVROT_1:33;
then (W-max (L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) <= (N-min (L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A2, A7, FINSEQ_6:98, SPRECT_5:24;
then A11: (W-max (L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) < (N-max (L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A7, A8, A10, SPRECT_5:25, XXREAL_0:2;
(N-max (L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) <= (E-max (L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A2, A7, A10, FINSEQ_6:98, SPRECT_5:26;
then A12: W-max (L~ (Cage C,n)) in rng (Upper_Seq C,n) by A3, A6, A10, A11, FINSEQ_5:49, XXREAL_0:2;
{(W-min (L~ (Cage C,n))),(W-max (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} c= rng (Upper_Seq C,n)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(W-min (L~ (Cage C,n))),(W-max (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} or x in rng (Upper_Seq C,n) )
assume x in {(W-min (L~ (Cage C,n))),(W-max (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} ; :: thesis: x in rng (Upper_Seq C,n)
hence x in rng (Upper_Seq C,n) by A5, A9, A12, ENUMSET1:def 1; :: thesis: verum

end;

then A13: card {(W-min (L~ (Cage C,n))),(W-max (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} c= card (rng (Upper_Seq C,n)) by CARD_1:27;
card (rng (Upper_Seq C,n)) c= card (dom (Upper_Seq C,n)) by CARD_2:80;
then A14: card (rng (Upper_Seq C,n)) c= len (Upper_Seq C,n) by CARD_1:104;
( W-min (L~ (Cage C,n)) <> W-max (L~ (Cage C,n)) & W-max (L~ (Cage C,n)) <> E-max (L~ (Cage C,n)) ) by JORDAN1B:6, SPRECT_2:62;
then card {(W-min (L~ (Cage C,n))),(W-max (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} = 3 by A1, CARD_2:77;
then 3 c= len (Upper_Seq C,n) by A13, A14, XBOOLE_1:1;
hence len (Upper_Seq C,n) >= 3 by NAT_1:40; :: thesis: len (Lower_Seq C,n) >= 3
A15: W-min (L~ (Cage C,n)) <> E-max (L~ (Cage C,n)) by TOPREAL5:25;
E-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:49;
then A16: E-min (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by FINSEQ_6:96, SPRECT_2:47;
(E-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 A2, A7, A10, FINSEQ_6:98, SPRECT_5:27;
then A17: E-min (L~ (Cage C,n)) in rng (Lower_Seq C,n) by A3, A16, FINSEQ_6:67;
{(W-min (L~ (Cage C,n))),(E-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} c= rng (Lower_Seq C,n)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(W-min (L~ (Cage C,n))),(E-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} or x in rng (Lower_Seq C,n) )
assume x in {(W-min (L~ (Cage C,n))),(E-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} ; :: thesis: x in rng (Lower_Seq C,n)
hence x in rng (Lower_Seq C,n) by A4, A17, ENUMSET1:def 1; :: thesis: verum

end;

then A18: card {(W-min (L~ (Cage C,n))),(E-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} c= card (rng (Lower_Seq C,n)) by CARD_1:27;
card (rng (Lower_Seq C,n)) c= card (dom (Lower_Seq C,n)) by CARD_2:80;
then A19: card (rng (Lower_Seq C,n)) c= len (Lower_Seq C,n) by CARD_1:104;
( W-min (L~ (Cage C,n)) <> E-min (L~ (Cage C,n)) & E-min (L~ (Cage C,n)) <> E-max (L~ (Cage C,n)) ) by Th18, SPRECT_2:58;
then card {(W-min (L~ (Cage C,n))),(E-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} = 3 by A15, CARD_2:77;
then 3 c= len (Lower_Seq C,n) by A18, A19, XBOOLE_1:1;
hence len (Lower_Seq C,n) >= 3 by NAT_1:40; :: thesis: verum