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