let n be Nat; for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( E-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & E-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ( E-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & E-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n)) )
set x = E-min (L~ (Cage (C,n)));
set p = E-max (L~ (Cage (C,n)));
set f = Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))));
A1:
rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = rng (Cage (C,n))
by FINSEQ_6:90, SPRECT_2:43;
A2:
E-min (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:45;
A3:
L~ (Cage (C,n)) = L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
by REVROT_1:33;
E-max (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:46;
then A4:
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;
A5:
E-max (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:46;
Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))
by JORDAN1E:def 1;
then
(Upper_Seq (C,n)) /. 1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1
by A4, FINSEQ_5:44;
then
(E-max (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) < (E-min (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
by A3, JORDAN1F:5, SPRECT_5:26;
then
E-min (L~ (Cage (C,n))) in rng ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n)))))
by A1, A2, A5, A3, FINSEQ_6:62;
hence A6:
E-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n))
by JORDAN1E:def 2; E-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n))
len (Lower_Seq (C,n)) >= 2
by TOPREAL1:def 8;
then
rng (Lower_Seq (C,n)) c= L~ (Lower_Seq (C,n))
by SPPOL_2:18;
hence
E-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n))
by A6; verum