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

( 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