let C be compact non horizontal non vertical Subset of (TOP-REAL 2); for n being Nat holds
( len (Upper_Seq (C,n)) >= 3 & len (Lower_Seq (C,n)) >= 3 )
let n be Nat; ( 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; 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; verum