let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( N-max (L~ (Cage C,n)) in rng (Upper_Seq C,n) & N-max (L~ (Cage C,n)) in L~ (Upper_Seq C,n) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( N-max (L~ (Cage C,n)) in rng (Upper_Seq C,n) & N-max (L~ (Cage C,n)) in L~ (Upper_Seq C,n) )
set x = N-max (L~ (Cage C,n));
set p = W-min (L~ (Cage C,n));
set f = Rotate (Cage C,n),(E-max (L~ (Cage C,n)));
A1:
rng (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) = rng (Cage C,n)
by FINSEQ_6:96, SPRECT_2:50;
A2:
N-max (L~ (Cage C,n)) in rng (Cage C,n)
by SPRECT_2:44;
A3:
W-min (L~ (Cage C,n)) in rng (Cage C,n)
by SPRECT_2:47;
A4:
Lower_Seq C,n = (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) -: (W-min (L~ (Cage C,n)))
by JORDAN1G:26;
W-min (L~ (Cage C,n)) in rng (Cage C,n)
by SPRECT_2:47;
then
W-min (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(E-max (L~ (Cage C,n))))
by FINSEQ_6:96, SPRECT_2:50;
then A5:
(Lower_Seq C,n) /. 1 = (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) /. 1
by A4, FINSEQ_5:47;
A6:
(Lower_Seq C,n) /. 1 = E-max (L~ (Cage C,n))
by JORDAN1F:6;
A7:
L~ (Cage C,n) = L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n))))
by REVROT_1:33;
then A8:
(W-min (L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) < (W-max (L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n))))
by A5, JORDAN1F:6, SPRECT_5:43;
A9:
(W-max (L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) <= (N-min (L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n))))
by A5, A7, JORDAN1F:6, SPRECT_5:44;
per cases
( N-max (L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n))))) <> E-max (L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n))))) or N-max (L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n))))) = E-max (L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n))))) )
;
suppose
N-max (L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n))))) <> E-max (L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))))
;
:: thesis: ( N-max (L~ (Cage C,n)) in rng (Upper_Seq C,n) & N-max (L~ (Cage C,n)) in L~ (Upper_Seq C,n) )then
(W-max (L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) < (N-max (L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n))))
by A5, A6, A7, A9, SPRECT_5:45, XXREAL_0:2;
then
N-max (L~ (Cage C,n)) in rng ((Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) :- (W-min (L~ (Cage C,n))))
by A1, A2, A3, A7, A8, FINSEQ_6:67, XXREAL_0:2;
hence A10:
N-max (L~ (Cage C,n)) in rng (Upper_Seq C,n)
by Th4;
:: thesis: N-max (L~ (Cage C,n)) in L~ (Upper_Seq C,n)
len (Upper_Seq C,n) >= 2
by TOPREAL1:def 10;
then
rng (Upper_Seq C,n) c= L~ (Upper_Seq C,n)
by SPPOL_2:18;
hence
N-max (L~ (Cage C,n)) in L~ (Upper_Seq C,n)
by A10;
:: thesis: verum end; suppose A11:
N-max (L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n))))) = E-max (L~ (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))))
;
:: thesis: ( N-max (L~ (Cage C,n)) in rng (Upper_Seq C,n) & N-max (L~ (Cage C,n)) in L~ (Upper_Seq C,n) )A12:
Upper_Seq C,
n = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n)))
by JORDAN1E:def 1;
E-max (L~ (Cage C,n)) in rng (Cage C,n)
by SPRECT_2:50;
then A13:
E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))
by FINSEQ_6:96, SPRECT_2:47;
(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))))
;
hence A14:
N-max (L~ (Cage C,n)) in rng (Upper_Seq C,n)
by A7, A11, A12, A13, FINSEQ_5:49;
:: thesis: N-max (L~ (Cage C,n)) in L~ (Upper_Seq C,n)
len (Upper_Seq C,n) >= 2
by TOPREAL1:def 10;
then
rng (Upper_Seq C,n) c= L~ (Upper_Seq C,n)
by SPPOL_2:18;
hence
N-max (L~ (Cage C,n)) in L~ (Upper_Seq C,n)
by A14;
:: thesis: verum end;