let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Upper_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: Upper_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: (Cage C,n) /. 1 = N-min (L~ (Cage C,n)) by JORDAN9:34;
A2: N-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:43;
A3: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
A4: E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
A5: (N-min (L~ (Cage C,n))) .. (Cage C,n) < (N-max (L~ (Cage C,n))) .. (Cage C,n) by A1, SPRECT_2:72;
A6: (N-max (L~ (Cage C,n))) .. (Cage C,n) <= (E-max (L~ (Cage C,n))) .. (Cage C,n) by A1, SPRECT_2:74;
A7: (N-min (L~ (Cage C,n))) .. (Cage C,n) < (E-max (L~ (Cage C,n))) .. (Cage C,n) by A1, A5, SPRECT_2:74, XXREAL_0:2;
A8: (E-min (L~ (Cage C,n))) .. (Cage C,n) <= (S-max (L~ (Cage C,n))) .. (Cage C,n) by A1, SPRECT_2:76;
A9: (S-min (L~ (Cage C,n))) .. (Cage C,n) <= (W-min (L~ (Cage C,n))) .. (Cage C,n) by A1, SPRECT_2:78;
(E-max (L~ (Cage C,n))) .. (Cage C,n) < (S-max (L~ (Cage C,n))) .. (Cage C,n) by A1, A8, SPRECT_2:75, XXREAL_0:2;
then A10: (E-max (L~ (Cage C,n))) .. (Cage C,n) < (S-min (L~ (Cage C,n))) .. (Cage C,n) by A1, SPRECT_2:77, XXREAL_0:2;
then A11: (E-max (L~ (Cage C,n))) .. (Cage C,n) < (W-min (L~ (Cage C,n))) .. (Cage C,n) by A1, SPRECT_2:78, XXREAL_0:2;
A12: E-max (L~ (Cage C,n)) in rng ((Cage C,n) -: (W-min (L~ (Cage C,n)))) by A3, A4, A9, A10, FINSEQ_5:49, XXREAL_0:2;
A13: (Cage C,n) -: (W-min (L~ (Cage C,n))) <> {} by A3, FINSEQ_5:50;
((Cage C,n) -: (W-min (L~ (Cage C,n)))) /. 1 = (Cage C,n) /. 1 by A3, FINSEQ_5:47
.= N-min (L~ (Cage C,n)) by JORDAN9:34 ;
then A14: N-min (L~ (Cage C,n)) in rng ((Cage C,n) -: (W-min (L~ (Cage C,n)))) by A13, FINSEQ_6:46;
len ((Cage C,n) -: (W-min (L~ (Cage C,n)))) = (W-min (L~ (Cage C,n))) .. (Cage C,n) by A3, FINSEQ_5:45;
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:48;
then A15: W-min (L~ (Cage C,n)) in rng ((Cage C,n) -: (W-min (L~ (Cage C,n)))) by A13, REVROT_1:3;
( 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:56, SPRECT_1:15;
then (W-max (L~ (Cage C,n))) `2 <= (N-min (L~ (Cage C,n))) `2 by PSCOMP_1:71;
then A16: N-min (L~ (Cage C,n)) <> W-min (L~ (Cage C,n)) by SPRECT_2:61;
then A17: card {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} = 2 by CARD_2:76;
{(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} c= rng ((Cage C,n) -: (W-min (L~ (Cage C,n))))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} or x in rng ((Cage C,n) -: (W-min (L~ (Cage C,n)))) )
assume x in {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} ; :: thesis: x in rng ((Cage C,n) -: (W-min (L~ (Cage C,n))))
hence x in rng ((Cage C,n) -: (W-min (L~ (Cage C,n)))) by A14, A15, TARSKI:def 2; :: thesis: verum

end;

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:27;
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:80;
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:104;
then 2 c= len ((Cage C,n) -: (W-min (L~ (Cage C,n)))) by A17, A18, XBOOLE_1:1;
then len ((Cage C,n) -: (W-min (L~ (Cage C,n)))) >= 2 by NAT_1:40;
then A19: 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;
A20: N-min (L~ (Cage C,n)) in rng ((Cage C,n) -: (W-min (L~ (Cage C,n)))) by A2, A3, A7, A11, FINSEQ_5:49, XXREAL_0:2;
A21: (E-max (L~ (Cage C,n))) .. ((Cage C,n) -: (W-min (L~ (Cage C,n)))) <> 1

proof

assume A22: (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 A2, A3, A7, A11, SPRECT_5:3, XXREAL_0:2
.= 1 by A1, FINSEQ_6:47 ;
hence contradiction by A5, A6, A12, A20, A22, FINSEQ_5:10; :: thesis: verum

end;

then A23: E-max (L~ (Cage C,n)) in rng (((Cage C,n) -: (W-min (L~ (Cage C,n)))) /^ 1) by A12, FINSEQ_6:83;
A24: (N-min (L~ (Cage C,n))) `1 < (N-max (L~ (Cage C,n))) `1 by SPRECT_2:55;
(N-max (L~ (Cage C,n))) `1 <= (NE-corner (L~ (Cage C,n))) `1 by PSCOMP_1:97;
then (N-max (L~ (Cage C,n))) `1 <= E-bound (L~ (Cage C,n)) by EUCLID:56;
then A25: N-min (L~ (Cage C,n)) <> E-max (L~ (Cage C,n)) by A24, EUCLID:56;
not E-max (L~ (Cage C,n)) in rng ((Cage C,n) :- (W-min (L~ (Cage C,n))))

proof

assume A26: E-max (L~ (Cage C,n)) in rng ((Cage C,n) :- (W-min (L~ (Cage C,n)))) ; :: thesis: contradiction
((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:57
.= (Cage C,n) /. 1 by FINSEQ_6:def 1
.= N-min (L~ (Cage C,n)) by JORDAN9:34 ;
then A27: N-min (L~ (Cage C,n)) in rng ((Cage C,n) :- (W-min (L~ (Cage C,n)))) by REVROT_1:3;
((Cage C,n) :- (W-min (L~ (Cage C,n)))) /. 1 = W-min (L~ (Cage C,n)) by FINSEQ_5:56;
then A28: W-min (L~ (Cage C,n)) in rng ((Cage C,n) :- (W-min (L~ (Cage C,n)))) by FINSEQ_6: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:56, SPRECT_1:15;
then (W-max (L~ (Cage C,n))) `2 <= (N-min (L~ (Cage C,n))) `2 by PSCOMP_1:71;
then N-min (L~ (Cage C,n)) <> W-min (L~ (Cage C,n)) by SPRECT_2:61;
then A29: card {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} = 2 by CARD_2:76;
{(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} c= rng ((Cage C,n) :- (W-min (L~ (Cage C,n))))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} or x in rng ((Cage C,n) :- (W-min (L~ (Cage C,n)))) )
assume x in {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} ; :: thesis: x in rng ((Cage C,n) :- (W-min (L~ (Cage C,n))))
hence x in rng ((Cage C,n) :- (W-min (L~ (Cage C,n)))) by A27, A28, TARSKI:def 2; :: thesis: verum

end;

then A30: 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:27;
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:80;
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:104;
then 2 c= len ((Cage C,n) :- (W-min (L~ (Cage C,n)))) by A29, A30, XBOOLE_1:1;
then len ((Cage C,n) :- (W-min (L~ (Cage C,n)))) >= 2 by NAT_1:40;
then 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;
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 A12, A19, A26, 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 JORDAN1G:25;
then E-max (L~ (Cage C,n)) = W-min (L~ (Cage C,n)) by A25, TARSKI:def 2;
hence contradiction by TOPREAL5:25; :: thesis: verum

end;

then A31: 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 A23, XBOOLE_0:def 5;
A32: W-min (L~ (Cage C,n)) in rng ((Cage C,n) :- (E-max (L~ (Cage C,n)))) by A3, A4, A9, A10, FINSEQ_6:67, XXREAL_0:2;
A33: card {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} = 2 by A25, CARD_2:76;
((Cage C,n) :- (E-max (L~ (Cage C,n)))) /. (len ((Cage C,n) :- (E-max (L~ (Cage C,n))))) = (Cage C,n) /. (len (Cage C,n)) by A4, FINSEQ_5:57
.= (Cage C,n) /. 1 by FINSEQ_6:def 1
.= N-min (L~ (Cage C,n)) by JORDAN9:34 ;
then A34: N-min (L~ (Cage C,n)) in rng ((Cage C,n) :- (E-max (L~ (Cage C,n)))) by REVROT_1:3;
((Cage C,n) :- (E-max (L~ (Cage C,n)))) /. 1 = E-max (L~ (Cage C,n)) by FINSEQ_5:56;
then A35: E-max (L~ (Cage C,n)) in rng ((Cage C,n) :- (E-max (L~ (Cage C,n)))) by FINSEQ_6:46;
{(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} c= rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} or x in rng ((Cage C,n) :- (E-max (L~ (Cage C,n)))) )
assume x in {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} ; :: thesis: x in rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))
hence x in rng ((Cage C,n) :- (E-max (L~ (Cage C,n)))) by A34, A35, TARSKI:def 2; :: thesis: verum

end;

then A36: card {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} c= card (rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))) by CARD_1:27;
card (rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))) c= card (dom ((Cage C,n) :- (E-max (L~ (Cage C,n))))) by CARD_2:80;
then card (rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))) c= len ((Cage C,n) :- (E-max (L~ (Cage C,n)))) by CARD_1:104;
then 2 c= len ((Cage C,n) :- (E-max (L~ (Cage C,n)))) by A33, A36, XBOOLE_1:1;
then len ((Cage C,n) :- (E-max (L~ (Cage C,n)))) >= 2 by NAT_1:40;
then A37: rng ((Cage C,n) :- (E-max (L~ (Cage C,n)))) c= L~ ((Cage C,n) :- (E-max (L~ (Cage C,n)))) by SPPOL_2:18;
not W-min (L~ (Cage C,n)) in rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))

proof

assume A38: W-min (L~ (Cage C,n)) in rng ((Cage C,n) -: (E-max (L~ (Cage C,n)))) ; :: thesis: contradiction
then A39: not (Cage C,n) -: (E-max (L~ (Cage C,n))) is empty by RELAT_1:60;
((Cage C,n) -: (E-max (L~ (Cage C,n)))) /. 1 = (Cage C,n) /. 1 by A4, FINSEQ_5:47
.= N-min (L~ (Cage C,n)) by JORDAN9:34 ;
then A40: N-min (L~ (Cage C,n)) in rng ((Cage C,n) -: (E-max (L~ (Cage C,n)))) by A39, FINSEQ_6:46;
((Cage C,n) -: (E-max (L~ (Cage C,n)))) /. (len ((Cage C,n) -: (E-max (L~ (Cage C,n))))) = ((Cage C,n) -: (E-max (L~ (Cage C,n)))) /. ((E-max (L~ (Cage C,n))) .. (Cage C,n)) by A4, FINSEQ_5:45
.= E-max (L~ (Cage C,n)) by A4, FINSEQ_5:48 ;
then A41: E-max (L~ (Cage C,n)) in rng ((Cage C,n) -: (E-max (L~ (Cage C,n)))) by A39, REVROT_1:3;
{(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} c= rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} or x in rng ((Cage C,n) -: (E-max (L~ (Cage C,n)))) )
assume x in {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} ; :: thesis: x in rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))
hence x in rng ((Cage C,n) -: (E-max (L~ (Cage C,n)))) by A40, A41, TARSKI:def 2; :: thesis: verum

end;

then A42: card {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} c= card (rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))) by CARD_1:27;
card (rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))) c= card (dom ((Cage C,n) -: (E-max (L~ (Cage C,n))))) by CARD_2:80;
then card (rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))) c= len ((Cage C,n) -: (E-max (L~ (Cage C,n)))) by CARD_1:104;
then 2 c= len ((Cage C,n) -: (E-max (L~ (Cage C,n)))) by A33, A42, XBOOLE_1:1;
then len ((Cage C,n) -: (E-max (L~ (Cage C,n)))) >= 2 by NAT_1:40;
then rng ((Cage C,n) -: (E-max (L~ (Cage C,n)))) c= L~ ((Cage C,n) -: (E-max (L~ (Cage C,n)))) by SPPOL_2:18;
then W-min (L~ (Cage C,n)) in (L~ ((Cage C,n) -: (E-max (L~ (Cage C,n))))) /\ (L~ ((Cage C,n) :- (E-max (L~ (Cage C,n))))) by A32, A37, A38, XBOOLE_0:def 4;
then W-min (L~ (Cage C,n)) in {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} by Th3;
then W-min (L~ (Cage C,n)) = E-max (L~ (Cage C,n)) by A16, TARSKI:def 2;
hence contradiction by TOPREAL5:25; :: thesis: verum

end;

then A43: W-min (L~ (Cage C,n)) in (rng (Cage C,n)) \ (rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))) by A3, XBOOLE_0:def 5;
(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)))) ^ ((((Cage C,n) -: (W-min (L~ (Cage C,n)))) /^ 1) -: (E-max (L~ (Cage C,n)))) by A31, FINSEQ_6:72
.= ((Cage C,n) :- (W-min (L~ (Cage C,n)))) ^ ((((Cage C,n) -: (W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n)))) /^ 1) by A12, A21, FINSEQ_6:65
.= (((Cage C,n) :- (E-max (L~ (Cage C,n)))) :- (W-min (L~ (Cage C,n)))) ^ ((((Cage C,n) -: (W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n)))) /^ 1) by A43, FINSEQ_6:76, SPRECT_2:50
.= (((Cage C,n) :- (E-max (L~ (Cage C,n)))) :- (W-min (L~ (Cage C,n)))) ^ (((Cage C,n) -: (E-max (L~ (Cage C,n)))) /^ 1) by A3, A12, FINSEQ_6:80
.= (((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 A32, FINSEQ_6:69
.= (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) :- (W-min (L~ (Cage C,n))) by A4, FINSEQ_6:def 2 ;
hence Upper_Seq C,n = (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) :- (W-min (L~ (Cage C,n))) by JORDAN1E:def 1; :: thesis: verum