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)))))

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 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

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)))))

proof

A21:
(N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n))
by A9, SPRECT_2:70;
((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) /. 1 = W-min (L~ (Cage (C,n)))
by FINSEQ_5:53;

then A16: W-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) by FINSEQ_6:42;

((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) /. (len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))) = (Cage (C,n)) /. (len (Cage (C,n))) by A3, FINSEQ_5:54

.= (Cage (C,n)) /. 1 by FINSEQ_6:def 1

.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;

then A17: N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) by FINSEQ_6:168;

{(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} c= rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) by A17, A16, TARSKI:def 2;

then A18: 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;

( 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 A19: card {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} = 2 by CARD_2:57;

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 A19, A18;

then len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) >= 2 by NAT_1:39;

then A20: 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;

assume E-max (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) ; :: thesis: contradiction

then E-max (L~ (Cage (C,n))) in (L~ ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))) by A13, A8, A20, XBOOLE_0:def 4;

then E-max (L~ (Cage (C,n))) in {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} by Th17;

then E-max (L~ (Cage (C,n))) = W-min (L~ (Cage (C,n))) by A14, TARSKI:def 2;

hence contradiction by TOPREAL5:19; :: thesis: verum

end;then A16: W-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) by FINSEQ_6:42;

((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) /. (len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))) = (Cage (C,n)) /. (len (Cage (C,n))) by A3, FINSEQ_5:54

.= (Cage (C,n)) /. 1 by FINSEQ_6:def 1

.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;

then A17: N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) by FINSEQ_6:168;

{(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} c= rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) by A17, A16, TARSKI:def 2;

then A18: 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;

( 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 A19: card {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} = 2 by CARD_2:57;

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 A19, A18;

then len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) >= 2 by NAT_1:39;

then A20: 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;

assume E-max (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) ; :: thesis: contradiction

then E-max (L~ (Cage (C,n))) in (L~ ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))) by A13, A8, A20, XBOOLE_0:def 4;

then E-max (L~ (Cage (C,n))) in {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} by Th17;

then E-max (L~ (Cage (C,n))) = W-min (L~ (Cage (C,n))) by A14, TARSKI:def 2;

hence contradiction by TOPREAL5:19; :: thesis: verum

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

proof

then
E-max (L~ (Cage (C,n))) in rng (((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /^ 1)
by A13, FINSEQ_6:78;
assume A26:
(E-max (L~ (Cage (C,n)))) .. ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) = 1
; :: thesis: contradiction

(N-min (L~ (Cage (C,n)))) .. ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) = (N-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A3, A23, A11, SPRECT_5:3, XXREAL_0:2

.= 1 by A9, FINSEQ_6:43 ;

hence contradiction by A22, A21, A13, A24, A26, FINSEQ_5:9; :: thesis: verum

end;(N-min (L~ (Cage (C,n)))) .. ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) = (N-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A3, A23, A11, SPRECT_5:3, XXREAL_0:2

.= 1 by A9, FINSEQ_6:43 ;

hence contradiction by A22, A21, A13, A24, A26, FINSEQ_5:9; :: thesis: verum

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