let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Nat holds
( len (Upper_Seq (C,n)) >= 3 & len (Lower_Seq (C,n)) >= 3 )
let n be 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:19;
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:43;
E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A3: 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;
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:54
.= (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:92 ;
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:61, 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 A5: E-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) by A3, FINSEQ_5:46;
W-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:44;
then A6: W-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
A7: (Upper_Seq (C,n)) /. 1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by A3, FINSEQ_5:44;
then A8: (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) by A2, FINSEQ_6:92;
then A9: W-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) by FINSEQ_6:42;
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:92, SPRECT_5:23;
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:24, 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:92, SPRECT_5:25;
then A12: W-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) by A3, A6, A10, A11, FINSEQ_5:46, 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)) by A5, A9, A12, ENUMSET1:def 1;
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:11;
card (rng (Upper_Seq (C,n))) c= card (dom (Upper_Seq (C,n))) by CARD_2:61;
then A14: card (rng (Upper_Seq (C,n))) c= len (Upper_Seq (C,n)) by CARD_1:62;
( 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:5, SPRECT_2:58;
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:58;
then Segm 3 c= Segm (len (Upper_Seq (C,n))) by A13, A14;
hence len (Upper_Seq (C,n)) >= 3 by NAT_1:39; :: thesis: len (Lower_Seq (C,n)) >= 3
A15: W-min (L~ (Cage (C,n))) <> E-max (L~ (Cage (C,n))) by TOPREAL5:19;
E-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:45;
then A16: E-min (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
(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:92, SPRECT_5:26;
then A17: E-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) by A3, A16, FINSEQ_6:62;
{(W-min (L~ (Cage (C,n)))),(E-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= rng (Lower_Seq (C,n)) by A4, A17, ENUMSET1:def 1;
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:11;
card (rng (Lower_Seq (C,n))) c= card (dom (Lower_Seq (C,n))) by CARD_2:61;
then A19: card (rng (Lower_Seq (C,n))) c= len (Lower_Seq (C,n)) by CARD_1:62;
( 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 Th14, SPRECT_2:54;
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:58;
then Segm 3 c= Segm (len (Lower_Seq (C,n))) by A18, A19;
hence len (Lower_Seq (C,n)) >= 3 by NAT_1:39; :: thesis: verum