let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) -: (W-min (L~ (Cage (C,n))))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) -: (W-min (L~ (Cage (C,n))))
set Nmi = N-min (L~ (Cage (C,n)));
set Nma = N-max (L~ (Cage (C,n)));
set Wmi = W-min (L~ (Cage (C,n)));
set Wma = W-max (L~ (Cage (C,n)));
set Ema = E-max (L~ (Cage (C,n)));
set Emi = E-min (L~ (Cage (C,n)));
set Sma = S-max (L~ (Cage (C,n)));
set Smi = S-min (L~ (Cage (C,n)));
set RotWmi = Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))));
set RotEma = Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))));
A1: E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
( W-max (L~ (Cage (C,n))) in L~ (Cage (C,n)) & (N-min (L~ (Cage (C,n)))) `2 = N-bound (L~ (Cage (C,n))) ) by EUCLID:52, SPRECT_1:13;
then (W-max (L~ (Cage (C,n)))) `2 <= (N-min (L~ (Cage (C,n)))) `2 by PSCOMP_1:24;
then N-min (L~ (Cage (C,n))) <> W-min (L~ (Cage (C,n))) by SPRECT_2:57;
then A2: card {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} = 2 by CARD_2:57;
A3: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
then A4: (Cage (C,n)) -: (W-min (L~ (Cage (C,n)))) <> {} by FINSEQ_5:47;
len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) = (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A3, FINSEQ_5:42;
then ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /. (len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))) = W-min (L~ (Cage (C,n))) by A3, FINSEQ_5:45;
then A5: W-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) by A4, FINSEQ_6:168;
((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /. 1 = (Cage (C,n)) /. 1 by A3, FINSEQ_5:44
.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;
then A6: N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) by A4, FINSEQ_6:42;
{(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} c= rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) by A6, A5, TARSKI:def 2;
then A7: card {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} c= card (rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))) by CARD_1:11;
card (rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))) c= card (dom ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))) by CARD_2:61;
then card (rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))) c= len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) by CARD_1:62;
then Segm 2 c= Segm (len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))) by A2, A7;
then len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) >= 2 by NAT_1:39;
then A8: rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) c= L~ ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) by SPPOL_2:18;
A9: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;
then (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:72;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A9, SPRECT_2:71, XXREAL_0:2;
then A10: (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A9, SPRECT_2:73, XXREAL_0:2;
then A11: (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A9, SPRECT_2:74, XXREAL_0:2;
A12: (S-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A9, SPRECT_2:74;
then A13: E-max (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) by A3, A1, A10, FINSEQ_5:46, XXREAL_0:2;
(N-max (L~ (Cage (C,n)))) `1 <= (NE-corner (L~ (Cage (C,n)))) `1 by PSCOMP_1:38;
then ( (N-min (L~ (Cage (C,n)))) `1 < (N-max (L~ (Cage (C,n)))) `1 & (N-max (L~ (Cage (C,n)))) `1 <= E-bound (L~ (Cage (C,n))) ) by EUCLID:52, SPRECT_2:51;
then A14: N-min (L~ (Cage (C,n))) <> E-max (L~ (Cage (C,n))) by EUCLID:52;
A15: not E-max (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) A21: (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A9, SPRECT_2:70;
A22: (N-min (L~ (Cage (C,n)))) .. (Cage (C,n)) < (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A9, SPRECT_2:68;
then A23: ( N-min (L~ (Cage (C,n))) in rng (Cage (C,n)) & (N-min (L~ (Cage (C,n)))) .. (Cage (C,n)) < (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) ) by A9, SPRECT_2:39, SPRECT_2:70, XXREAL_0:2;
then A24: N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) by A3, A11, FINSEQ_5:46, XXREAL_0:2;
A25: (E-max (L~ (Cage (C,n)))) .. ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) <> 1 then E-max (L~ (Cage (C,n))) in rng (((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /^ 1) by A13, FINSEQ_6:78;
then A27: E-max (L~ (Cage (C,n))) in (rng (((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /^ 1)) \ (rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))) by A15, XBOOLE_0:def 5;
A28: W-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) by A3, A1, A12, A10, FINSEQ_6:62, XXREAL_0:2;
(Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n)))) = (((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) ^ (((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /^ 1)) :- (E-max (L~ (Cage (C,n)))) by A3, FINSEQ_6:def 2
.= (((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /^ 1) :- (E-max (L~ (Cage (C,n)))) by A27, FINSEQ_6:65
.= ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) :- (E-max (L~ (Cage (C,n)))) by A13, A25, FINSEQ_6:83
.= ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) -: (W-min (L~ (Cage (C,n)))) by A3, A1, A12, A10, Th16, XXREAL_0:2
.= (((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) ^ (((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) /^ 1)) -: (W-min (L~ (Cage (C,n)))) by A28, FINSEQ_6:66
.= (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) -: (W-min (L~ (Cage (C,n)))) by A1, FINSEQ_6:def 2 ;
hence Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) -: (W-min (L~ (Cage (C,n)))) by JORDAN1E:def 2; :: thesis: verum