:: Again on the Order on a Special Polygon
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 16, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, FINSEQ_1, FINSEQ_6, SUBSET_1, RELAT_1,
FINSEQ_4, XXREAL_0, FINSEQ_5, ARYTM_1, ARYTM_3, ORDINAL4, RFINSEQ,
PARTFUN1, FUNCT_1, GOBOARD5, PRE_TOPC, EUCLID, CARD_1, PSCOMP_1,
TOPREAL1, SPRECT_2, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, RFINSEQ, FINSEQ_6,
NAT_1, NAT_D, PRE_TOPC, EUCLID, TOPREAL1, GOBOARD5, PSCOMP_1, SPRECT_2;
constructors FINSEQ_4, RFINSEQ, FINSEQ_5, GOBOARD5, PSCOMP_1, SPRECT_2, NAT_D,
RELSET_1;
registrations XBOOLE_0, RELSET_1, XREAL_0, FINSEQ_6, STRUCT_0, SPRECT_2,
REVROT_1, ORDINAL1, FUNCT_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions FUNCT_1;
theorems FINSEQ_6, FINSEQ_4, FINSEQ_5, FINSEQ_3, NAT_1, FINSEQ_1, TARSKI,
GOBOARD7, RFINSEQ, REVROT_1, SPRECT_2, XBOOLE_0, XREAL_1, XXREAL_0,
PARTFUN1, CARD_1;
begin
reserve D for non empty set,
f for FinSequence of D,
g for circular FinSequence of D,
p,p1,p2,p3,q for Element of D;
theorem Th1:
q in rng(f|(p..f)) implies q..f <= p..f
proof
assume
A1: q in rng(f|(p..f));
then q..(f|(p..f)) = q..f by FINSEQ_5:40;
then
A2: q..f <= len(f|(p..f)) by A1,FINSEQ_4:21;
len(f|(p..f)) <= p..f by FINSEQ_5:17;
hence thesis by A2,XXREAL_0:2;
end;
theorem Th2:
p in rng f & q in rng f & p..f <= q..f implies q..(f:-p) = q..f - p..f + 1
proof
assume that
A1: p in rng f and
A2: q in rng f and
A3: p..f <= q..f;
A4: f = (f|(p..f))^(f/^(p..f)) by RFINSEQ:8;
per cases by A3,XXREAL_0:1;
suppose
p..f = q..f;
then p = q by A1,A2,FINSEQ_5:9;
hence thesis by FINSEQ_6:79;
end;
suppose
A5: p..f < q..f;
p..f <= len f by A1,FINSEQ_4:21;
then
A6: len(f|(p..f)) = p..f by FINSEQ_1:59;
A7: not q in rng(f|(p..f)) by A5,Th1;
q in rng(f|(p..f)) \/ rng(f/^(p..f)) by A2,A4,FINSEQ_1:31;
then
A8: q in rng(f/^(p..f)) by A7,XBOOLE_0:def 3;
then q in rng(f/^(p..f)) \ rng(f|(p..f)) by A7,XBOOLE_0:def 5;
then
A9: q..f = p..f + q..(f/^(p..f)) by A4,A6,FINSEQ_6:7;
not q in {p} by A5,TARSKI:def 1;
then not q in rng<*p*> by FINSEQ_1:38;
then
A10: q in rng(f/^(p..f)) \ rng<*p*> by A8,XBOOLE_0:def 5;
f:-p = <*p*>^(f/^p..f) by FINSEQ_5:def 2;
hence q..(f:-p) = len<*p*> + q..(f/^(p..f)) by A10,FINSEQ_6:7
.= q..f - p..f + 1 by A9,FINSEQ_1:39;
end;
end;
theorem Th3:
p in rng f & q in rng f & p..f <= q..f implies p..(f-:q) = p..f
proof
A1: f-:q = f|(q..f) by FINSEQ_5:def 1;
assume p in rng f & q in rng f & p..f <= q..f;
then p in rng(f|(q..f)) by A1,FINSEQ_5:46;
hence thesis by A1,FINSEQ_5:40;
end;
theorem Th4:
p in rng f & q in rng f & p..f <= q..f implies q..Rotate(f,p) = q
..f - p..f + 1
proof
assume that
A1: p in rng f and
A2: q in rng f;
A3: Rotate(f,p) = (f:-p)^((f-:p)/^1) by A1,FINSEQ_6:def 2;
assume
A4: p..f <= q..f;
then q in rng(f:-p) by A1,A2,FINSEQ_6:62;
hence q..Rotate(f,p) = q..(f:-p) by A3,FINSEQ_6:6
.= q..f - p..f + 1 by A1,A2,A4,Th2;
end;
theorem Th5:
p1 in rng f & p2 in rng f & p3 in rng f & p1..f <= p2..f & p2..f
< p3..f implies p2..Rotate(f,p1) < p3..Rotate(f,p1)
proof
assume that
A1: p1 in rng f & p2 in rng f & p3 in rng f & p1..f <= p2..f and
A2: p2..f < p3..f;
A3: p2..f - p1..f < p3..f - p1..f by A2,XREAL_1:9;
p2..Rotate(f,p1) = p2..f - p1..f + 1 & p3..Rotate(f,p1) = p3..f - p1..f
+ 1 by A1,A2,Th4,XXREAL_0:2;
hence thesis by A3,XREAL_1:6;
end;
theorem
p1 in rng f & p2 in rng f & p3 in rng f & p1..f < p2..f & p2..f <= p3
..f implies p2..Rotate(f,p1) <= p3..Rotate(f,p1)
proof
assume that
A1: p1 in rng f and
A2: p2 in rng f & p3 in rng f and
A3: p1..f < p2..f and
A4: p2..f <= p3..f;
per cases by A4,XXREAL_0:1;
suppose
p2..f < p3..f;
hence thesis by A1,A2,A3,Th5;
end;
suppose
p2..f = p3..f;
hence thesis by A2,FINSEQ_5:9;
end;
end;
theorem Th7:
p in rng g & len g > 1 implies p..g < len g
proof
assume that
A1: p in rng g and
A2: len g > 1 and
A3: p..g >= len g;
p..g <= len g by A1,FINSEQ_4:21;
then p..g = len g by A3,XXREAL_0:1;
then
A4: p = g/.len g by A1,FINSEQ_5:38
.= g/.1 by FINSEQ_6:def 1;
g is non empty by A2,CARD_1:27;
hence contradiction by A2,A3,A4,FINSEQ_6:43;
end;
begin :: Ordering of special points on a standard special sequence
reserve f for non constant standard special_circular_sequence,
p,p1,p2,p3,q for Point of TOP-REAL 2;
registration
let f;
cluster f/^1 -> one-to-one;
coherence
proof
let x1,x2 be object such that
A1: x1 in dom(f/^1) and
A2: x2 in dom (f/^1) and
A3: (f/^1).x1 = (f/^1).x2;
reconsider i=x1, j=x2 as Nat by A1,A2;
1 <= i by A1,FINSEQ_3:25;
then
A4: 1 < i+1 by NAT_1:13;
i+1 in dom f by A1,FINSEQ_5:26;
then
A5: i+1 <= len f by FINSEQ_3:25;
1 <= j by A2,FINSEQ_3:25;
then
A6: 1 < j+1 by NAT_1:13;
j+1 in dom f by A2,FINSEQ_5:26;
then
A7: j+1 <= len f by FINSEQ_3:25;
assume
A8: x1 <> x2;
per cases by A8,XXREAL_0:1;
suppose
i < j;
then
A9: i+1 < j+1 by XREAL_1:6;
f/.(i+1) = (f/^1)/.i by A1,FINSEQ_5:27
.= (f/^1).j by A1,A3,PARTFUN1:def 6
.= (f/^1)/.j by A2,PARTFUN1:def 6
.= f/.(j+1) by A2,FINSEQ_5:27;
hence contradiction by A4,A7,A9,GOBOARD7:37;
end;
suppose
j < i;
then
A10: j+1 < i+1 by XREAL_1:6;
f/.(j+1) = (f/^1)/.j by A2,FINSEQ_5:27
.= (f/^1).i by A2,A3,PARTFUN1:def 6
.= (f/^1)/.i by A1,PARTFUN1:def 6
.= f/.(i+1) by A1,FINSEQ_5:27;
hence contradiction by A5,A6,A10,GOBOARD7:37;
end;
end;
end;
theorem Th8:
1 < q..f & q in rng f implies (f/.1)..Rotate(f,q) = len f + 1 - q ..f
proof
assume that
A1: 1 < q..f and
A2: q in rng f;
set i = 1 + len f -' q..f;
A3: q..f - 1 > 0 by A1,XREAL_1:50;
A4: q..f <= len f by A2,FINSEQ_4:21;
then
A5: q..f <= len f + 1 by NAT_1:13;
then
A6: i = 1 + len f - q..f by XREAL_1:233;
then i +(q..f - 1) = len f;
then i < len f by A3,XREAL_1:29;
then
A7: i < len Rotate(f,q) by FINSEQ_6:179;
now
assume q..f + 0 >= len f;
then
A8: q..f = len f by A4,XXREAL_0:1;
q = f/.(q..f) by A2,FINSEQ_5:38
.= f/.1 by A8,FINSEQ_6:def 1;
hence contradiction by A1,FINSEQ_6:43;
end;
then
A9: len f - q..f > 0 by XREAL_1:20;
i = 1 + (len f - q..f) by A6;
then
A10: 1 + 0 < i by A9,XREAL_1:6;
then
A11: i in dom Rotate(f,q) by A7,FINSEQ_3:25;
A12: f/.1 = Rotate(f,q)/.(1 + len f -' q..f) by A1,A2,FINSEQ_6:183;
then
A13: f/.1 = Rotate(f,q).i by A11,PARTFUN1:def 6;
for j being object st j in dom Rotate(f,q) & j <> i
holds Rotate(f,q).j <> f/.1
proof
let z be object;
assume that
A14: z in dom Rotate(f,q) and
A15: z <> i;
reconsider j = z as Nat by A14;
per cases by A15,XXREAL_0:1;
suppose
A16: j < i;
1 <= j by A14,FINSEQ_3:25;
then Rotate(f,q)/.j <> f/.1 by A12,A7,A16,GOBOARD7:36;
hence thesis by A14,PARTFUN1:def 6;
end;
suppose
A17: i < j;
j <= len Rotate(f,q) by A14,FINSEQ_3:25;
then Rotate(f,q)/.j <> f/.1 by A12,A10,A17,GOBOARD7:37;
hence thesis by A14,PARTFUN1:def 6;
end;
end;
then
A18: Rotate(f,q) just_once_values f/.1 by A11,A13,FINSEQ_4:7;
then 1 + len f -' q..f = Rotate(f,q) <- (f/.1) by A11,A13,FINSEQ_4:def 3;
hence f/.1..Rotate(f,q) = 1 + len f -' q..f by A18,FINSEQ_4:25
.= len f + 1 - q..f by A5,XREAL_1:233;
end;
theorem Th9:
p in rng f & q in rng f & p..f < q..f implies p..Rotate(f,q) =
len f + p..f - q..f
proof
assume that
A1: p in rng f and
A2: q in rng f;
assume
A3: p..f < q..f;
then
A4: p..f = p..(f-:q) by A1,A2,Th3;
A5: p in rng(f-:q) by A1,A2,A3,FINSEQ_5:46;
then
A6: p..(f-:q) >= 1 by FINSEQ_4:21;
A7: Rotate(f,q) = (f:-q)^((f-:q)/^1) by A2,FINSEQ_6:def 2;
per cases by A6,A4,XXREAL_0:1;
suppose
A8: p..f = 1;
then p = f/.1 by A1,FINSEQ_5:38;
hence thesis by A2,A3,A8,Th8;
end;
suppose
A9: p..f > 1;
then
A10: p..f = 1 + p..((f-:q)/^1) by A5,A4,FINSEQ_6:56;
not p in {q} by A3,TARSKI:def 1;
then
A11: not p in rng<*q*> by FINSEQ_1:38;
A12: q in rng(f/^1) by A2,A3,A9,FINSEQ_6:78;
then ((f/^1) -| q)^<*q*> = (f/^1)|(q..(f/^1)) by FINSEQ_5:24
.= (f/^1)-:q by FINSEQ_5:def 1;
then
A13: rng((f/^1)-:q) = rng((f/^1) -| q) \/ rng<*q*> by FINSEQ_1:31;
A14: rng((f/^1) -| q) misses rng((f/^1) |-- q) by A12,FINSEQ_4:57;
(f/^1):-q = <*q*>^((f/^1) |-- q) by A12,FINSEQ_6:41;
then
A15: rng((f/^1):-q) = rng<*q*> \/ rng((f/^1) |-- q) by FINSEQ_1:31;
p..(f-:q) > 1 by A1,A2,A3,A9,Th3;
then
A16: p in rng((f-:q)/^1) by A5,FINSEQ_6:57;
then p in rng((f/^1)-:q) by A2,A3,A9,FINSEQ_6:60;
then p in rng((f/^1) -| q) by A13,A11,XBOOLE_0:def 3;
then not p in rng((f/^1) |-- q) by A14,XBOOLE_0:3;
then not p in rng((f/^1):-q) by A11,A15,XBOOLE_0:def 3;
then not p in rng(f:-q) by A2,A3,A9,FINSEQ_6:83;
then p in rng((f-:q)/^1) \ rng(f:-q) by A16,XBOOLE_0:def 5;
hence p..Rotate(f,q) = len(f:-q) + p..((f-:q)/^1) by A7,FINSEQ_6:7
.= len f - q..f + 1 + (p..f - 1) by A2,A10,FINSEQ_5:50
.= len f + p..f - q..f;
end;
end;
theorem Th10:
p1 in rng f & p2 in rng f & p3 in rng f & p1..f < p2..f & p2..f
< p3..f implies p3..Rotate(f,p2) < p1..Rotate(f,p2)
proof
assume that
A1: p1 in rng f and
A2: p2 in rng f and
A3: p3 in rng f and
A4: p1..f < p2..f and
A5: p2..f < p3..f;
A6: p1 in rng Rotate(f,p2) & p3 in rng Rotate(f,p2) by A1,A2,A3,FINSEQ_6:90;
1 <= p1..f & p3..f <= len f by A1,A3,FINSEQ_4:21;
then
A7: p3..f + 1 <= len f + p1..f by XREAL_1:7;
A8: p3..Rotate(f,p2) = p3..f - p2..f + 1 by A2,A3,A5,Th4
.= p3..f + 1 - p2..f;
p1..Rotate(f,p2) = len f + p1..f - p2..f by A1,A2,A4,Th9;
then p3..Rotate(f,p2) <= p1..Rotate(f,p2) by A8,A7,XREAL_1:9;
hence thesis by A4,A5,A6,FINSEQ_5:9,XXREAL_0:1;
end;
theorem Th11:
p1 in rng f & p2 in rng f & p3 in rng f & p1..f < p2..f & p2..f
< p3..f implies p1..Rotate(f,p3) < p2..Rotate(f,p3)
proof
assume that
A1: p1 in rng f and
A2: p2 in rng f and
A3: p3 in rng f and
A4: p1..f < p2..f & p2..f < p3..f;
p1..f < p3..f by A4,XXREAL_0:2;
then
A5: p1..Rotate(f,p3) = len f + p1..f - p3..f by A1,A3,Th9;
p2..Rotate(f,p3) = len f + p2..f - p3..f & len f + p1..f < len f + p2..f
by A2,A3,A4,Th9,XREAL_1:6;
hence thesis by A5,XREAL_1:9;
end;
theorem
p1 in rng f & p2 in rng f & p3 in rng f & p1..f <= p2..f & p2..f < p3
..f implies p1..Rotate(f,p3) <= p2..Rotate(f,p3)
proof
assume that
A1: p1 in rng f & p2 in rng f and
A2: p3 in rng f and
A3: p1..f <= p2..f and
A4: p2..f < p3..f;
per cases by A3,XXREAL_0:1;
suppose
p1..f < p2..f;
hence thesis by A1,A2,A4,Th11;
end;
suppose
p1..f = p2..f;
hence thesis by A1,FINSEQ_5:9;
end;
end;
theorem
(S-min L~f)..f < len f
proof
S-min L~f in rng f & len f > 1 by GOBOARD7:34,SPRECT_2:41,XXREAL_0:2;
hence thesis by Th7;
end;
theorem
(S-max L~f)..f < len f
proof
S-max L~f in rng f & len f > 1 by GOBOARD7:34,SPRECT_2:42,XXREAL_0:2;
hence thesis by Th7;
end;
theorem
(E-min L~f)..f < len f
proof
E-min L~f in rng f & len f > 1 by GOBOARD7:34,SPRECT_2:45,XXREAL_0:2;
hence thesis by Th7;
end;
theorem
(E-max L~f)..f < len f
proof
E-max L~f in rng f & len f > 1 by GOBOARD7:34,SPRECT_2:46,XXREAL_0:2;
hence thesis by Th7;
end;
theorem
(N-min L~f)..f < len f
proof
N-min L~f in rng f & len f > 1 by GOBOARD7:34,SPRECT_2:39,XXREAL_0:2;
hence thesis by Th7;
end;
theorem
(N-max L~f)..f < len f
proof
N-max L~f in rng f & len f > 1 by GOBOARD7:34,SPRECT_2:40,XXREAL_0:2;
hence thesis by Th7;
end;
theorem
(W-max L~f)..f < len f
proof
W-max L~f in rng f & len f > 1 by GOBOARD7:34,SPRECT_2:44,XXREAL_0:2;
hence thesis by Th7;
end;
theorem
(W-min L~f)..f < len f
proof
W-min L~f in rng f & len f > 1 by GOBOARD7:34,SPRECT_2:43,XXREAL_0:2;
hence thesis by Th7;
end;
begin :: Ordering of special points on a clockwise oriented sequence
reserve z for clockwise_oriented non constant standard
special_circular_sequence;
Lm1: z/.1 = N-min L~z implies (E-max L~z)..z < (S-max L~z)..z
proof
assume
A1: z/.1 = N-min L~z;
then
(E-max L~z)..z < (E-min L~z)..z by SPRECT_2:71;
hence thesis by A1,SPRECT_2:72,XXREAL_0:2;
end;
Lm2: z/.1 = N-min L~z implies (E-max L~z)..z < (S-min L~z)..z
proof
assume
A1: z/.1 = N-min L~z;
then (E-max L~z)..z < (S-max L~z)..z by Lm1;
hence thesis by A1,SPRECT_2:73,XXREAL_0:2;
end;
Lm3: z/.1 = N-min L~z implies (E-max L~z)..z < (W-min L~z)..z
proof
assume
A1: z/.1 = N-min L~z;
then
(E-max L~z)..z < (S-min L~z)..z by Lm2;
hence thesis by A1,SPRECT_2:74,XXREAL_0:2;
end;
Lm4: z/.1 = N-min L~z implies (E-min L~z)..z < (S-min L~z)..z
proof
assume
A1: z/.1 = N-min L~z;
then
(S-max L~z)..z < (S-min L~z)..z by SPRECT_2:73;
hence thesis by A1,SPRECT_2:72,XXREAL_0:2;
end;
Lm5: z/.1 = N-min L~z implies (E-min L~z)..z < (W-min L~z)..z
proof
assume
A1: z/.1 = N-min L~z;
then
(E-min L~z)..z < (S-min L~z)..z by Lm4;
hence thesis by A1,SPRECT_2:74,XXREAL_0:2;
end;
Lm6: z/.1 = N-min L~z implies (S-max L~z)..z < (W-min L~z)..z
proof
assume
A1: z/.1 = N-min L~z;
then
(S-max L~z)..z < (S-min L~z)..z by SPRECT_2:73;
hence thesis by A1,SPRECT_2:74,XXREAL_0:2;
end;
Lm7: z/.1 = N-min L~z implies (N-max L~z)..z < (W-min L~z)..z
proof
assume
A1: z/.1 = N-min L~z;
then
(E-max L~z)..z < (W-min L~z)..z by Lm3;
hence thesis by A1,SPRECT_2:70,XXREAL_0:2;
end;
Lm8: z/.1 = N-min L~z implies (N-min L~z)..z < (W-min L~z)..z
proof
assume
A1: z/.1 = N-min L~z;
then (N-max L~z)..z < (W-min L~z)..z by Lm7;
hence thesis by A1,SPRECT_2:68,XXREAL_0:2;
end;
Lm9: z/.1 = N-min L~z implies (N-max L~z)..z < (S-max L~z)..z
proof
assume
A1: z/.1 = N-min L~z;
then (N-max L~z)..z <= (E-max L~z)..z by SPRECT_2:70;
hence thesis by A1,Lm1,XXREAL_0:2;
end;
Lm10: z/.1 = N-min L~z implies (N-max L~z)..z < (S-min L~z)..z
proof
assume
A1: z/.1 = N-min L~z;
then (N-max L~z)..z < (S-max L~z)..z by Lm9;
hence thesis by A1,SPRECT_2:73,XXREAL_0:2;
end;
theorem Th21:
f/.1 = W-min L~f implies (W-min L~f)..f < (W-max L~f)..f
proof
assume f/.1 = W-min L~f;
then
A1: (W-min L~f)..f = 1 by FINSEQ_6:43;
A2: W-max L~f in rng f by SPRECT_2:44;
then (W-max L~f)..f in dom f by FINSEQ_4:20;
then
A3: (W-max L~f)..f >= 1 by FINSEQ_3:25;
W-min L~f in rng f by SPRECT_2:43;
then (W-min L~f)..f <> (W-max L~f)..f by A2,FINSEQ_5:9,SPRECT_2:58;
hence thesis by A3,A1,XXREAL_0:1;
end;
theorem
f/.1 = W-min L~f implies (W-max L~f)..f > 1
proof
assume
A1: f/.1 = W-min L~f;
then (W-min L~f)..f = 1 by FINSEQ_6:43;
hence thesis by A1,Th21;
end;
theorem Th23:
z/.1 = W-min L~z & W-max L~z <> N-min L~z implies (W-max L~z)..z
< (N-min L~z)..z
proof
set g = Rotate(z,N-min L~z);
A1: L~z = L~g by REVROT_1:33;
N-min L~z in rng z by SPRECT_2:39;
then
A2: g/.1 = N-min L~g by A1,FINSEQ_6:92;
then
A3: (W-min L~g)..g > (N-min L~g)..g by Lm8;
assume that
A4: z/.1 = W-min L~z and
A5: W-max L~z <> N-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,W-min L~z) = z by A4,FINSEQ_6:181;
A7: N-min L~g in rng g & W-max L~g in rng g by SPRECT_2:39,44;
W-min L~g in rng g & (W-min L~g)..g < (W-max L~g)..g by A1,A5,A2,SPRECT_2:43
,75;
hence thesis by A1,A6,A7,A3,Th10;
end;
theorem Th24:
z/.1 = W-min L~z implies (N-min L~z)..z < (N-max L~z)..z
proof
set g = Rotate(z,N-min L~z);
A1: L~z = L~g by REVROT_1:33;
N-min L~z in rng z by SPRECT_2:39;
then g/.1 = N-min L~g by A1,FINSEQ_6:92;
then
A2: (N-min L~g)..g < (N-max L~g)..g & (N-max L~g)..g < (W-min L~g)..g by Lm7,
SPRECT_2:68;
A3: W-min L~g in rng g by SPRECT_2:43;
assume
A4: z/.1 = W-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,W-min L~z) = z by A4,FINSEQ_6:181;
N-min L~g in rng g & N-max L~g in rng g by SPRECT_2:39,40;
hence thesis by A1,A5,A3,A2,Th11;
end;
theorem Th25:
z/.1 = W-min L~z & N-max L~z <> E-max L~z implies (N-max L~z)..z
< (E-max L~z)..z
proof
set g = Rotate(z,N-min L~z);
A1: L~z = L~g by REVROT_1:33;
N-min L~z in rng z by SPRECT_2:39;
then
A2: g/.1 = N-min L~g by A1,FINSEQ_6:92;
then
A3: (E-max L~g)..g < (W-min L~g)..g by Lm3;
assume that
A4: z/.1 = W-min L~z and
A5: N-max L~z <> E-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,W-min L~z) = z by A4,FINSEQ_6:181;
A7: N-max L~g in rng g & E-max L~g in rng g by SPRECT_2:40,46;
W-min L~g in rng g & (N-max L~g)..g < (E-max L~g)..g by A1,A5,A2,SPRECT_2:43
,70;
hence thesis by A1,A6,A7,A3,Th11;
end;
theorem Th26:
z/.1 = W-min L~z implies (E-max L~z)..z < (E-min L~z)..z
proof
set g = Rotate(z,N-min L~z);
A1: L~z = L~g by REVROT_1:33;
N-min L~z in rng z by SPRECT_2:39;
then g/.1 = N-min L~g by A1,FINSEQ_6:92;
then
A2: (E-max L~g)..g < (E-min L~g)..g & (E-min L~g)..g < (W-min L~g)..g by Lm5,
SPRECT_2:71;
A3: W-min L~g in rng g by SPRECT_2:43;
assume
A4: z/.1 = W-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,W-min L~z) = z by A4,FINSEQ_6:181;
E-min L~g in rng g & E-max L~g in rng g by SPRECT_2:45,46;
hence thesis by A1,A5,A3,A2,Th11;
end;
theorem Th27:
z/.1 = W-min L~z & E-min L~z <> S-max L~z implies (E-min L~z)..z
< (S-max L~z)..z
proof
set g = Rotate(z,N-min L~z);
A1: L~z = L~g by REVROT_1:33;
N-min L~z in rng z by SPRECT_2:39;
then
A2: g/.1 = N-min L~g by A1,FINSEQ_6:92;
then
A3: (S-max L~g)..g < (W-min L~g)..g by Lm6;
assume that
A4: z/.1 = W-min L~z and
A5: E-min L~z <> S-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,W-min L~z) = z by A4,FINSEQ_6:181;
A7: E-min L~g in rng g & S-max L~g in rng g by SPRECT_2:42,45;
W-min L~g in rng g & (E-min L~g)..g < (S-max L~g)..g by A1,A5,A2,SPRECT_2:43
,72;
hence thesis by A1,A6,A7,A3,Th11;
end;
theorem
z/.1 = W-min L~z & S-min L~z <> W-min L~z implies (S-max L~z)..z < (
S-min L~z)..z
proof
set g = Rotate(z,N-min L~z);
A1: L~z = L~g by REVROT_1:33;
assume
A2: z/.1 = W-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A3: Rotate(g,W-min L~z) = z by A2,FINSEQ_6:181;
A4: S-min L~g in rng g & S-max L~g in rng g by SPRECT_2:41,42;
N-min L~z in rng z by SPRECT_2:39;
then
A5: g/.1 = N-min L~g by A1,FINSEQ_6:92;
then
A6: W-min L~g in rng g & (S-max L~g)..g < (S-min L~g)..g by SPRECT_2:43,73;
assume S-min L~z <> W-min L~z;
then (S-min L~g)..g < (W-min L~g)..g by A1,A5,SPRECT_2:74;
hence thesis by A1,A3,A4,A6,Th11;
end;
theorem Th29:
f/.1 = S-max L~f implies (S-max L~f)..f < (S-min L~f)..f
proof
assume f/.1 = S-max L~f;
then
A1: (S-max L~f)..f = 1 by FINSEQ_6:43;
A2: S-min L~f in rng f by SPRECT_2:41;
then (S-min L~f)..f in dom f by FINSEQ_4:20;
then
A3: (S-min L~f)..f >= 1 by FINSEQ_3:25;
S-max L~f in rng f by SPRECT_2:42;
then (S-max L~f)..f <> (S-min L~f)..f by A2,FINSEQ_5:9,SPRECT_2:56;
hence thesis by A3,A1,XXREAL_0:1;
end;
theorem
f/.1 = S-max L~f implies (S-min L~f)..f > 1
proof
assume
A1: f/.1 = S-max L~f;
then (S-max L~f)..f = 1 by FINSEQ_6:43;
hence thesis by A1,Th29;
end;
Lm11: z/.1 = W-min L~z implies (E-max L~z)..z < (S-max L~z)..z
proof
assume
A1: z/.1 = W-min L~z;
then
(E-max L~z)..z < (E-min L~z)..z by Th26;
hence thesis by A1,Th27,XXREAL_0:2;
end;
Lm12: z/.1 = W-min L~z implies (N-min L~z)..z < (E-max L~z)..z
proof
assume
A1: z/.1 = W-min L~z;
then
(N-min L~z)..z < (N-max L~z)..z by Th24;
hence thesis by A1,Th25,XXREAL_0:2;
end;
Lm13: z/.1 = W-min L~z implies (N-min L~z)..z < (S-max L~z)..z
proof
assume
A1: z/.1 = W-min L~z;
then (N-min L~z)..z < (E-max L~z)..z by Lm12;
hence thesis by A1,Lm11,XXREAL_0:2;
end;
Lm14: z/.1 = W-min L~z implies (N-max L~z)..z < (S-max L~z)..z
proof
assume
A1: z/.1 = W-min L~z;
then
(E-max L~z)..z < (S-max L~z)..z by Lm11;
hence thesis by A1,Th25,XXREAL_0:2;
end;
Lm15: z/.1 = W-min L~z implies (W-max L~z)..z < (S-max L~z)..z
proof
assume
A1: z/.1 = W-min L~z;
then
(N-min L~z)..z < (S-max L~z)..z by Lm13;
hence thesis by A1,Th23,XXREAL_0:2;
end;
Lm16: z/.1 = W-min L~z implies (N-max L~z)..z < (E-min L~z)..z
proof
assume
A1: z/.1 = W-min L~z;
then
(E-max L~z)..z < (E-min L~z)..z by Th26;
hence thesis by A1,Th25,XXREAL_0:2;
end;
Lm17: z/.1 = W-min L~z implies (N-min L~z)..z < (E-max L~z)..z
proof
assume
A1: z/.1 = W-min L~z;
then
(N-min L~z)..z < (N-max L~z)..z by Th24;
hence thesis by A1,Th25,XXREAL_0:2;
end;
Lm18: z/.1 = W-min L~z implies (W-max L~z)..z < (E-max L~z)..z
proof
assume
A1: z/.1 = W-min L~z;
then (W-max L~z)..z <= (N-min L~z)..z by Th23;
hence thesis by A1,Lm17,XXREAL_0:2;
end;
Lm19: z/.1 = W-min L~z implies (W-max L~z)..z < (E-min L~z)..z
proof
assume
A1: z/.1 = W-min L~z;
then (W-max L~z)..z < (E-max L~z)..z by Lm18;
hence thesis by A1,Th26,XXREAL_0:2;
end;
theorem Th31:
z/.1 = S-max L~z & S-min L~z <> W-min L~z implies (S-min L~z)..z
< (W-min L~z)..z
proof
set g = Rotate(z,N-min L~z);
A1: L~z = L~g by REVROT_1:33;
N-min L~z in rng z by SPRECT_2:39;
then
A2: g/.1 = N-min L~g by A1,FINSEQ_6:92;
then
A3: S-min L~g in rng g & (S-max L~g)..g < (S-min L~g)..g by SPRECT_2:41,73;
assume that
A4: z/.1 = S-max L~z and
A5: S-min L~z <> W-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,S-max L~z) = z by A4,FINSEQ_6:181;
A7: W-min L~g in rng g & S-max L~g in rng g by SPRECT_2:42,43;
(S-min L~g)..g < (W-min L~g)..g by A1,A5,A2,SPRECT_2:74;
hence thesis by A1,A6,A7,A3,Th5;
end;
theorem Th32:
z/.1 = S-max L~z implies (W-min L~z)..z < (W-max L~z)..z
proof
set g = Rotate(z,W-min L~z);
A1: L~z = L~g by REVROT_1:33;
W-min L~z in rng z by SPRECT_2:43;
then g/.1 = W-min L~g by A1,FINSEQ_6:92;
then
A2: (S-max L~g)..g > (W-max L~g)..g & (W-min L~g)..g < (W-max L~g)..g by Lm15
,Th21;
A3: W-min L~g in rng g by SPRECT_2:43;
assume
A4: z/.1 = S-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,S-max L~z) = z by A4,FINSEQ_6:181;
S-max L~g in rng g & W-max L~g in rng g by SPRECT_2:42,44;
hence thesis by A1,A5,A3,A2,Th11;
end;
theorem Th33:
z/.1 = S-max L~z & W-max L~z <> N-min L~z implies (W-max L~z)..z
< (N-min L~z)..z
proof
set g = Rotate(z,W-min L~z);
A1: L~z = L~g by REVROT_1:33;
W-min L~z in rng z by SPRECT_2:43;
then
A2: g/.1 = W-min L~g by A1,FINSEQ_6:92;
then
A3: (N-min L~g)..g < (S-max L~g)..g by Lm13;
assume that
A4: z/.1 = S-max L~z and
A5: W-max L~z <> N-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,S-max L~z) = z by A4,FINSEQ_6:181;
A7: W-max L~g in rng g & N-min L~g in rng g by SPRECT_2:39,44;
S-max L~g in rng g & (W-max L~g)..g < (N-min L~g)..g by A1,A5,A2,Th23,
SPRECT_2:42;
hence thesis by A1,A6,A7,A3,Th11;
end;
theorem Th34:
z/.1 = S-max L~z implies (N-min L~z)..z < (N-max L~z)..z
proof
set g = Rotate(z,W-min L~z);
A1: L~z = L~g by REVROT_1:33;
W-min L~z in rng z by SPRECT_2:43;
then g/.1 = W-min L~g by A1,FINSEQ_6:92;
then
A2: (N-min L~g)..g < (N-max L~g)..g & (N-max L~g)..g < (S-max L~g)..g by Lm14
,Th24;
A3: S-max L~g in rng g by SPRECT_2:42;
assume
A4: z/.1 = S-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,S-max L~z) = z by A4,FINSEQ_6:181;
N-max L~g in rng g & N-min L~g in rng g by SPRECT_2:39,40;
hence thesis by A1,A5,A3,A2,Th11;
end;
theorem Th35:
z/.1 = S-max L~z & N-max L~z <> E-max L~z implies (N-max L~z)..z
< (E-max L~z)..z
proof
set g = Rotate(z,W-min L~z);
A1: L~z = L~g by REVROT_1:33;
W-min L~z in rng z by SPRECT_2:43;
then
A2: g/.1 = W-min L~g by A1,FINSEQ_6:92;
then
A3: (E-max L~g)..g < (S-max L~g)..g by Lm11;
assume that
A4: z/.1 = S-max L~z and
A5: N-max L~z <> E-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,S-max L~z) = z by A4,FINSEQ_6:181;
A7: N-max L~g in rng g & E-max L~g in rng g by SPRECT_2:40,46;
S-max L~g in rng g & (N-max L~g)..g < (E-max L~g)..g by A1,A5,A2,Th25,
SPRECT_2:42;
hence thesis by A1,A6,A7,A3,Th11;
end;
theorem
z/.1 = S-max L~z & E-min L~z <> S-max L~z implies (E-max L~z)..z < (
E-min L~z)..z
proof
set g = Rotate(z,W-min L~z);
A1: L~z = L~g by REVROT_1:33;
assume
A2: z/.1 = S-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A3: Rotate(g,S-max L~z) = z by A2,FINSEQ_6:181;
A4: E-min L~g in rng g & E-max L~g in rng g by SPRECT_2:45,46;
W-min L~z in rng z by SPRECT_2:43;
then
A5: g/.1 = W-min L~g by A1,FINSEQ_6:92;
then
A6: S-max L~g in rng g & (E-max L~g)..g < (E-min L~g)..g by Th26,SPRECT_2:42;
assume E-min L~z <> S-max L~z;
then (E-min L~g)..g < (S-max L~g)..g by A1,A5,Th27;
hence thesis by A1,A3,A4,A6,Th11;
end;
theorem Th37:
f/.1 = E-max L~f implies (E-max L~f)..f < (E-min L~f)..f
proof
assume f/.1 = E-max L~f;
then
A1: (E-max L~f)..f = 1 by FINSEQ_6:43;
A2: E-min L~f in rng f by SPRECT_2:45;
then (E-min L~f)..f in dom f by FINSEQ_4:20;
then
A3: (E-min L~f)..f >= 1 by FINSEQ_3:25;
E-max L~f in rng f by SPRECT_2:46;
then (E-min L~f)..f <> (E-max L~f)..f by A2,FINSEQ_5:9,SPRECT_2:54;
hence thesis by A3,A1,XXREAL_0:1;
end;
theorem
f/.1 = E-max L~f implies (E-min L~f)..f > 1
proof
assume
A1: f/.1 = E-max L~f;
then (E-max L~f)..f = 1 by FINSEQ_6:43;
hence thesis by A1,Th37;
end;
theorem Th39:
z/.1 = E-max L~z & S-max L~z <> E-min L~z implies (E-min L~z)..z
< (S-max L~z)..z
proof
set g = Rotate(z,N-min L~z);
A1: L~z = L~g by REVROT_1:33;
N-min L~z in rng z by SPRECT_2:39;
then
A2: g/.1 = N-min L~g by A1,FINSEQ_6:92;
then
A3: E-min L~g in rng g & (E-max L~g)..g < (E-min L~g)..g by SPRECT_2:45,71;
assume that
A4: z/.1 = E-max L~z and
A5: S-max L~z <> E-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,E-max L~z) = z by A4,FINSEQ_6:181;
A7: S-max L~g in rng g & E-max L~g in rng g by SPRECT_2:42,46;
(E-min L~g)..g < (S-max L~g)..g by A1,A5,A2,SPRECT_2:72;
hence thesis by A1,A6,A7,A3,Th5;
end;
theorem Th40:
z/.1 = E-max L~z implies (S-max L~z)..z < (S-min L~z)..z
proof
set g = Rotate(z,N-min L~z);
A1: L~z = L~g by REVROT_1:33;
N-min L~z in rng z by SPRECT_2:39;
then g/.1 = N-min L~g by A1,FINSEQ_6:92;
then
A2: (E-max L~g)..g < (S-max L~g)..g & (S-max L~g)..g < (S-min L~g)..g by Lm1,
SPRECT_2:73;
A3: S-min L~g in rng g by SPRECT_2:41;
assume
A4: z/.1 = E-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,E-max L~z) = z by A4,FINSEQ_6:181;
S-max L~g in rng g & E-max L~g in rng g by SPRECT_2:42,46;
hence thesis by A1,A5,A3,A2,Th5;
end;
Lm20: z/.1 = S-max L~z implies (N-min L~z)..z < (E-max L~z)..z
proof
assume
A1: z/.1 = S-max L~z;
then
(N-min L~z)..z < (N-max L~z)..z by Th34;
hence thesis by A1,Th35,XXREAL_0:2;
end;
Lm21: z/.1 = S-max L~z implies (W-max L~z)..z < (E-max L~z)..z
proof
assume
A1: z/.1 = S-max L~z;
then
(N-min L~z)..z < (E-max L~z)..z by Lm20;
hence thesis by A1,Th33,XXREAL_0:2;
end;
Lm22: z/.1 = S-max L~z implies (W-min L~z)..z < (E-max L~z)..z
proof
assume
A1: z/.1 = S-max L~z;
then (W-min L~z)..z < (W-max L~z)..z by Th32;
hence thesis by A1,Lm21,XXREAL_0:2;
end;
Lm23: z/.1 = S-max L~z implies (W-max L~z)..z < (N-max L~z)..z
proof
assume
A1: z/.1 = S-max L~z;
then
(N-min L~z)..z < (N-max L~z)..z by Th34;
hence thesis by A1,Th33,XXREAL_0:2;
end;
Lm24: z/.1 = S-max L~z implies (W-min L~z)..z < (N-min L~z)..z
proof
assume
A1: z/.1 = S-max L~z;
then
(W-min L~z)..z < (W-max L~z)..z by Th32;
hence thesis by A1,Th33,XXREAL_0:2;
end;
Lm25: z/.1 = S-max L~z implies (S-min L~z)..z < (N-min L~z)..z
proof
assume
A1: z/.1 = S-max L~z;
then (S-min L~z)..z <= (W-min L~z)..z by Th31;
hence thesis by A1,Lm24,XXREAL_0:2;
end;
Lm26: z/.1 = S-max L~z implies (S-min L~z)..z < (N-max L~z)..z
proof
assume
A1: z/.1 = S-max L~z;
then (S-min L~z)..z < (N-min L~z)..z by Lm25;
hence thesis by A1,Th34,XXREAL_0:2;
end;
theorem Th41:
z/.1 = E-max L~z & S-min L~z <> W-min L~z implies (S-min L~z)..z
< (W-min L~z)..z
proof
set g = Rotate(z,S-max L~z);
A1: L~z = L~g by REVROT_1:33;
S-max L~z in rng z by SPRECT_2:42;
then
A2: g/.1 = S-max L~g by A1,FINSEQ_6:92;
then
A3: (W-min L~g)..g < (E-max L~g)..g by Lm22;
assume that
A4: z/.1 = E-max L~z and
A5: S-min L~z <> W-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,E-max L~z) = z by A4,FINSEQ_6:181;
A7: S-min L~g in rng g & W-min L~g in rng g by SPRECT_2:41,43;
E-max L~g in rng g & (S-min L~g)..g < (W-min L~g)..g by A1,A5,A2,Th31,
SPRECT_2:46;
hence thesis by A1,A6,A7,A3,Th11;
end;
theorem Th42:
z/.1 = E-max L~z implies (W-min L~z)..z < (W-max L~z)..z
proof
set g = Rotate(z,S-max L~z);
A1: L~z = L~g by REVROT_1:33;
S-max L~z in rng z by SPRECT_2:42;
then g/.1 = S-max L~g by A1,FINSEQ_6:92;
then
A2: (W-min L~g)..g < (W-max L~g)..g & (W-max L~g)..g < (E-max L~g)..g by Lm21
,Th32;
A3: E-max L~g in rng g by SPRECT_2:46;
assume
A4: z/.1 = E-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,E-max L~z) = z by A4,FINSEQ_6:181;
W-max L~g in rng g & W-min L~g in rng g by SPRECT_2:43,44;
hence thesis by A1,A5,A3,A2,Th11;
end;
theorem Th43:
z/.1 = E-max L~z & W-max L~z <> N-min L~z implies (W-max L~z)..z
< (N-min L~z)..z
proof
set g = Rotate(z,S-max L~z);
A1: L~z = L~g by REVROT_1:33;
S-max L~z in rng z by SPRECT_2:42;
then
A2: g/.1 = S-max L~g by A1,FINSEQ_6:92;
then
A3: (N-min L~g)..g < (E-max L~g)..g by Lm20;
assume that
A4: z/.1 = E-max L~z and
A5: W-max L~z <> N-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,E-max L~z) = z by A4,FINSEQ_6:181;
A7: W-max L~g in rng g & N-min L~g in rng g by SPRECT_2:39,44;
E-max L~g in rng g & (W-max L~g)..g < (N-min L~g)..g by A1,A5,A2,Th33,
SPRECT_2:46;
hence thesis by A1,A6,A7,A3,Th11;
end;
theorem
z/.1 = E-max L~z & N-max L~z <> E-max L~z implies (N-min L~z)..z < (
N-max L~z)..z
proof
set g = Rotate(z,S-max L~z);
A1: L~z = L~g by REVROT_1:33;
assume
A2: z/.1 = E-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A3: Rotate(g,E-max L~z) = z by A2,FINSEQ_6:181;
A4: N-max L~g in rng g & N-min L~g in rng g by SPRECT_2:39,40;
S-max L~z in rng z by SPRECT_2:42;
then
A5: g/.1 = S-max L~g by A1,FINSEQ_6:92;
then
A6: E-max L~g in rng g & (N-min L~g)..g < (N-max L~g)..g by Th34,SPRECT_2:46;
assume N-max L~z <> E-max L~z;
then (N-max L~g)..g < (E-max L~g)..g by A1,A5,Th35;
hence thesis by A1,A3,A4,A6,Th11;
end;
theorem
f/.1 = N-max L~f & N-max L~f <> E-max L~f implies (N-max L~f)..f < (
E-max L~f)..f
proof
assume that
A1: f/.1 = N-max L~f and
A2: N-max L~f <> E-max L~f;
A3: E-max L~f in rng f by SPRECT_2:46;
then (E-max L~f)..f in dom f by FINSEQ_4:20;
then
A4: (E-max L~f)..f >= 1 by FINSEQ_3:25;
N-max L~f in rng f & (N-max L~f)..f = 1 by A1,FINSEQ_6:43,SPRECT_2:40;
hence thesis by A3,A2,A4,FINSEQ_5:9,XXREAL_0:1;
end;
theorem
z/.1 = N-max L~z implies (E-max L~z)..z < (E-min L~z)..z
proof
set g = Rotate(z,W-min L~z);
A1: L~z = L~g by REVROT_1:33;
W-min L~z in rng z by SPRECT_2:43;
then g/.1 = W-min L~g by A1,FINSEQ_6:92;
then
A2: (N-max L~g)..g <= (E-max L~g)..g & (E-max L~g)..g < (E-min L~g)..g by Th25
,Th26;
A3: E-max L~g in rng g by SPRECT_2:46;
assume
A4: z/.1 = N-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,N-max L~z) = z by A4,FINSEQ_6:181;
E-min L~g in rng g & N-max L~g in rng g by SPRECT_2:40,45;
hence thesis by A1,A5,A3,A2,Th5;
end;
theorem
z/.1 = N-max L~z & E-min L~z <> S-max L~z implies (E-min L~z)..z < (
S-max L~z)..z
proof
set g = Rotate(z,W-min L~z);
A1: L~z = L~g by REVROT_1:33;
W-min L~z in rng z by SPRECT_2:43;
then
A2: g/.1 = W-min L~g by A1,FINSEQ_6:92;
then
A3: S-max L~g in rng g & (N-max L~g)..g < (E-min L~g)..g by Lm16,SPRECT_2:42;
assume that
A4: z/.1 = N-max L~z and
A5: E-min L~z <> S-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,N-max L~z) = z by A4,FINSEQ_6:181;
A7: E-min L~g in rng g & N-max L~g in rng g by SPRECT_2:40,45;
(E-min L~g)..g < (S-max L~g)..g by A1,A5,A2,Th27;
hence thesis by A1,A6,A7,A3,Th5;
end;
theorem
z/.1 = N-max L~z implies (S-max L~z)..z < (S-min L~z)..z
proof
set g = Rotate(z,N-min L~z);
A1: L~z = L~g by REVROT_1:33;
N-min L~z in rng z by SPRECT_2:39;
then g/.1 = N-min L~g by A1,FINSEQ_6:92;
then
A2: (S-max L~g)..g < (S-min L~g)..g & (N-max L~g)..g < (S-max L~g)..g by Lm9,
SPRECT_2:73;
A3: N-max L~g in rng g by SPRECT_2:40;
assume
A4: z/.1 = N-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,N-max L~z) = z by A4,FINSEQ_6:181;
S-max L~g in rng g & S-min L~g in rng g by SPRECT_2:41,42;
hence thesis by A1,A5,A3,A2,Th5;
end;
theorem
z/.1 = N-max L~z & S-min L~z <> W-min L~z implies (S-min L~z)..z < (
W-min L~z)..z
proof
set g = Rotate(z,N-min L~z);
A1: L~z = L~g by REVROT_1:33;
N-min L~z in rng z by SPRECT_2:39;
then
A2: g/.1 = N-min L~g by A1,FINSEQ_6:92;
then
A3: (N-max L~g)..g < (S-min L~g)..g by Lm10;
assume that
A4: z/.1 = N-max L~z and
A5: S-min L~z <> W-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,N-max L~z) = z by A4,FINSEQ_6:181;
A7: W-min L~g in rng g & S-min L~g in rng g by SPRECT_2:41,43;
N-max L~g in rng g & (S-min L~g)..g < (W-min L~g)..g by A1,A5,A2,SPRECT_2:40
,74;
hence thesis by A1,A6,A7,A3,Th5;
end;
theorem
z/.1 = N-max L~z implies (W-min L~z)..z < (W-max L~z)..z
proof
set g = Rotate(z,S-max L~z);
A1: L~z = L~g by REVROT_1:33;
S-max L~z in rng z by SPRECT_2:42;
then g/.1 = S-max L~g by A1,FINSEQ_6:92;
then
A2: (W-min L~g)..g < (W-max L~g)..g & (W-max L~g)..g < (N-max L~g)..g by Lm23
,Th32;
A3: N-max L~g in rng g by SPRECT_2:40;
assume
A4: z/.1 = N-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,N-max L~z) = z by A4,FINSEQ_6:181;
W-min L~g in rng g & W-max L~g in rng g by SPRECT_2:43,44;
hence thesis by A1,A5,A3,A2,Th11;
end;
theorem
z/.1 = N-max L~z & N-min L~z <> W-max L~z implies (W-max L~z)..z < (
N-min L~z)..z
proof
set g = Rotate(z,S-max L~z);
A1: L~z = L~g by REVROT_1:33;
S-max L~z in rng z by SPRECT_2:42;
then
A2: g/.1 = S-max L~g by A1,FINSEQ_6:92;
then
A3: (N-min L~g)..g < (N-max L~g)..g by Th34;
assume that
A4: z/.1 = N-max L~z and
A5: N-min L~z <> W-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,N-max L~z) = z by A4,FINSEQ_6:181;
A7: N-min L~g in rng g & W-max L~g in rng g by SPRECT_2:39,44;
N-max L~g in rng g & (W-max L~g)..g < (N-min L~g)..g by A1,A5,A2,Th33,
SPRECT_2:40;
hence thesis by A1,A6,A7,A3,Th11;
end;
theorem
f/.1 = E-min L~f & E-min L~f <> S-max L~f implies (E-min L~f)..f < (
S-max L~f)..f
proof
assume that
A1: f/.1 = E-min L~f and
A2: E-min L~f <> S-max L~f;
A3: S-max L~f in rng f by SPRECT_2:42;
then (S-max L~f)..f in dom f by FINSEQ_4:20;
then
A4: (S-max L~f)..f >= 1 by FINSEQ_3:25;
E-min L~f in rng f & (E-min L~f)..f = 1 by A1,FINSEQ_6:43,SPRECT_2:45;
hence thesis by A3,A2,A4,FINSEQ_5:9,XXREAL_0:1;
end;
theorem
z/.1 = E-min L~z implies (S-max L~z)..z < (S-min L~z)..z
proof
set g = Rotate(z,N-min L~z);
A1: L~z = L~g by REVROT_1:33;
N-min L~z in rng z by SPRECT_2:39;
then g/.1 = N-min L~g by A1,FINSEQ_6:92;
then
A2: (E-min L~g)..g <= (S-max L~g)..g & (S-max L~g)..g < (S-min L~g)..g by
SPRECT_2:72,73;
A3: S-max L~g in rng g by SPRECT_2:42;
assume
A4: z/.1 = E-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,E-min L~z) = z by A4,FINSEQ_6:181;
S-min L~g in rng g & E-min L~g in rng g by SPRECT_2:41,45;
hence thesis by A1,A5,A3,A2,Th5;
end;
theorem
z/.1 = E-min L~z & S-min L~z <> W-min L~z implies (S-min L~z)..z < (
W-min L~z)..z
proof
set g = Rotate(z,N-min L~z);
A1: L~z = L~g by REVROT_1:33;
N-min L~z in rng z by SPRECT_2:39;
then
A2: g/.1 = N-min L~g by A1,FINSEQ_6:92;
then
A3: W-min L~g in rng g & (E-min L~g)..g < (S-min L~g)..g by Lm4,SPRECT_2:43;
assume that
A4: z/.1 = E-min L~z and
A5: S-min L~z <> W-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,E-min L~z) = z by A4,FINSEQ_6:181;
A7: S-min L~g in rng g & E-min L~g in rng g by SPRECT_2:41,45;
(S-min L~g)..g < (W-min L~g)..g by A1,A5,A2,SPRECT_2:74;
hence thesis by A1,A6,A7,A3,Th5;
end;
Lm27: z/.1 = E-max L~z implies (S-max L~z)..z < (W-min L~z)..z
proof
assume
A1: z/.1 = E-max L~z;
then
(S-max L~z)..z < (S-min L~z)..z by Th40;
hence thesis by A1,Th41,XXREAL_0:2;
end;
Lm28: z/.1 = E-max L~z implies (E-min L~z)..z < (W-min L~z)..z
proof
assume
A1: z/.1 = E-max L~z;
then (E-min L~z)..z <= (S-max L~z)..z by Th39;
hence thesis by A1,Lm27,XXREAL_0:2;
end;
Lm29: z/.1 = E-max L~z implies (E-min L~z)..z < (W-max L~z)..z
proof
assume
A1: z/.1 = E-max L~z;
then (E-min L~z)..z < (W-min L~z)..z by Lm28;
hence thesis by A1,Th42,XXREAL_0:2;
end;
Lm30: z/.1 = E-max L~z implies (S-min L~z)..z < (W-max L~z)..z
proof
assume
A1: z/.1 = E-max L~z;
then
(W-min L~z)..z < (W-max L~z)..z by Th42;
hence thesis by A1,Th41,XXREAL_0:2;
end;
theorem
z/.1 = E-min L~z implies (W-min L~z)..z < (W-max L~z)..z
proof
set g = Rotate(z,E-max L~z);
A1: L~z = L~g by REVROT_1:33;
E-max L~z in rng z by SPRECT_2:46;
then g/.1 = E-max L~g by A1,FINSEQ_6:92;
then
A2: (W-min L~g)..g < (W-max L~g)..g & (E-min L~g)..g < (W-min L~g)..g by Lm28
,Th42;
A3: E-min L~g in rng g by SPRECT_2:45;
assume
A4: z/.1 = E-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,E-min L~z) = z by A4,FINSEQ_6:181;
W-min L~g in rng g & W-max L~g in rng g by SPRECT_2:43,44;
hence thesis by A1,A5,A3,A2,Th5;
end;
theorem
z/.1 = E-min L~z & W-max L~z <> N-min L~z implies (W-max L~z)..z < (
N-min L~z)..z
proof
set g = Rotate(z,E-max L~z);
A1: L~z = L~g by REVROT_1:33;
E-max L~z in rng z by SPRECT_2:46;
then
A2: g/.1 = E-max L~g by A1,FINSEQ_6:92;
then
A3: (E-min L~g)..g < (W-max L~g)..g by Lm29;
assume that
A4: z/.1 = E-min L~z and
A5: W-max L~z <> N-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,E-min L~z) = z by A4,FINSEQ_6:181;
A7: N-min L~g in rng g & W-max L~g in rng g by SPRECT_2:39,44;
E-min L~g in rng g & (W-max L~g)..g < (N-min L~g)..g by A1,A5,A2,Th43,
SPRECT_2:45;
hence thesis by A1,A6,A7,A3,Th5;
end;
theorem
z/.1 = E-min L~z implies (N-min L~z)..z < (N-max L~z)..z
proof
set g = Rotate(z,W-min L~z);
A1: L~z = L~g by REVROT_1:33;
W-min L~z in rng z by SPRECT_2:43;
then g/.1 = W-min L~g by A1,FINSEQ_6:92;
then
A2: (N-min L~g)..g < (N-max L~g)..g & (N-max L~g)..g < (E-min L~g)..g by Lm16
,Th24;
A3: E-min L~g in rng g by SPRECT_2:45;
assume
A4: z/.1 = E-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,E-min L~z) = z by A4,FINSEQ_6:181;
N-min L~g in rng g & N-max L~g in rng g by SPRECT_2:39,40;
hence thesis by A1,A5,A3,A2,Th11;
end;
theorem
z/.1 = E-min L~z & E-max L~z <> N-max L~z implies (N-max L~z)..z < (
E-max L~z)..z
proof
set g = Rotate(z,W-min L~z);
A1: L~z = L~g by REVROT_1:33;
W-min L~z in rng z by SPRECT_2:43;
then
A2: g/.1 = W-min L~g by A1,FINSEQ_6:92;
then
A3: (E-max L~g)..g < (E-min L~g)..g by Th26;
assume that
A4: z/.1 = E-min L~z and
A5: E-max L~z <> N-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,E-min L~z) = z by A4,FINSEQ_6:181;
A7: E-max L~g in rng g & N-max L~g in rng g by SPRECT_2:40,46;
E-min L~g in rng g & (N-max L~g)..g < (E-max L~g)..g by A1,A5,A2,Th25,
SPRECT_2:45;
hence thesis by A1,A6,A7,A3,Th11;
end;
theorem
f/.1 = S-min L~f & S-min L~f <> W-min L~f implies (S-min L~f)..f < (
W-min L~f)..f
proof
assume that
A1: f/.1 = S-min L~f and
A2: S-min L~f <> W-min L~f;
A3: W-min L~f in rng f by SPRECT_2:43;
then (W-min L~f)..f in dom f by FINSEQ_4:20;
then
A4: (W-min L~f)..f >= 1 by FINSEQ_3:25;
S-min L~f in rng f & (S-min L~f)..f = 1 by A1,FINSEQ_6:43,SPRECT_2:41;
hence thesis by A3,A2,A4,FINSEQ_5:9,XXREAL_0:1;
end;
theorem
z/.1 = S-min L~z implies (W-min L~z)..z < (W-max L~z)..z
proof
set g = Rotate(z,E-max L~z);
A1: L~z = L~g by REVROT_1:33;
E-max L~z in rng z by SPRECT_2:46;
then g/.1 = E-max L~g by A1,FINSEQ_6:92;
then
A2: (S-min L~g)..g <= (W-min L~g)..g & (W-min L~g)..g < (W-max L~g)..g by Th41
,Th42;
A3: W-min L~g in rng g by SPRECT_2:43;
assume
A4: z/.1 = S-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,S-min L~z) = z by A4,FINSEQ_6:181;
W-max L~g in rng g & S-min L~g in rng g by SPRECT_2:41,44;
hence thesis by A1,A5,A3,A2,Th5;
end;
theorem
z/.1 = S-min L~z & W-max L~z <> N-min L~z implies (W-max L~z)..z < (
N-min L~z)..z
proof
set g = Rotate(z,E-max L~z);
A1: L~z = L~g by REVROT_1:33;
E-max L~z in rng z by SPRECT_2:46;
then
A2: g/.1 = E-max L~g by A1,FINSEQ_6:92;
then
A3: N-min L~g in rng g & (S-min L~g)..g < (W-max L~g)..g by Lm30,SPRECT_2:39;
assume that
A4: z/.1 = S-min L~z and
A5: W-max L~z <> N-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,S-min L~z) = z by A4,FINSEQ_6:181;
A7: W-max L~g in rng g & S-min L~g in rng g by SPRECT_2:41,44;
(W-max L~g)..g < (N-min L~g)..g by A1,A5,A2,Th43;
hence thesis by A1,A6,A7,A3,Th5;
end;
theorem
z/.1 = S-min L~z implies (N-min L~z)..z < (N-max L~z)..z
proof
set g = Rotate(z,S-max L~z);
A1: L~z = L~g by REVROT_1:33;
S-max L~z in rng z by SPRECT_2:42;
then g/.1 = S-max L~g by A1,FINSEQ_6:92;
then
A2: (N-min L~g)..g < (N-max L~g)..g & (S-min L~g)..g < (N-min L~g)..g by Lm25
,Th34;
A3: S-min L~g in rng g by SPRECT_2:41;
assume
A4: z/.1 = S-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,S-min L~z) = z by A4,FINSEQ_6:181;
N-min L~g in rng g & N-max L~g in rng g by SPRECT_2:39,40;
hence thesis by A1,A5,A3,A2,Th5;
end;
theorem
z/.1 = S-min L~z & N-max L~z <> E-max L~z implies (N-max L~z)..z < (
E-max L~z)..z
proof
set g = Rotate(z,S-max L~z);
A1: L~z = L~g by REVROT_1:33;
S-max L~z in rng z by SPRECT_2:42;
then
A2: g/.1 = S-max L~g by A1,FINSEQ_6:92;
then
A3: (S-min L~g)..g < (N-max L~g)..g by Lm26;
assume that
A4: z/.1 = S-min L~z and
A5: N-max L~z <> E-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,S-min L~z) = z by A4,FINSEQ_6:181;
A7: E-max L~g in rng g & N-max L~g in rng g by SPRECT_2:40,46;
S-min L~g in rng g & (N-max L~g)..g < (E-max L~g)..g by A1,A5,A2,Th35,
SPRECT_2:41;
hence thesis by A1,A6,A7,A3,Th5;
end;
theorem
z/.1 = S-min L~z implies (E-max L~z)..z < (E-min L~z)..z
proof
set g = Rotate(z,N-min L~z);
A1: L~z = L~g by REVROT_1:33;
N-min L~z in rng z by SPRECT_2:39;
then g/.1 = N-min L~g by A1,FINSEQ_6:92;
then
A2: (E-max L~g)..g < (E-min L~g)..g & (E-min L~g)..g < (S-min L~g)..g by Lm4,
SPRECT_2:71;
A3: S-min L~g in rng g by SPRECT_2:41;
assume
A4: z/.1 = S-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,S-min L~z) = z by A4,FINSEQ_6:181;
E-max L~g in rng g & E-min L~g in rng g by SPRECT_2:45,46;
hence thesis by A1,A5,A3,A2,Th11;
end;
theorem
z/.1 = S-min L~z & S-max L~z <> E-min L~z implies (E-min L~z)..z < (
S-max L~z)..z
proof
set g = Rotate(z,N-min L~z);
A1: L~z = L~g by REVROT_1:33;
N-min L~z in rng z by SPRECT_2:39;
then
A2: g/.1 = N-min L~g by A1,FINSEQ_6:92;
then
A3: (S-max L~g)..g < (S-min L~g)..g by SPRECT_2:73;
assume that
A4: z/.1 = S-min L~z and
A5: S-max L~z <> E-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,S-min L~z) = z by A4,FINSEQ_6:181;
A7: S-max L~g in rng g & E-min L~g in rng g by SPRECT_2:42,45;
S-min L~g in rng g & (E-min L~g)..g < (S-max L~g)..g by A1,A5,A2,SPRECT_2:41
,72;
hence thesis by A1,A6,A7,A3,Th11;
end;
theorem
f/.1 = W-max L~f & W-max L~f <> N-min L~f implies (W-max L~f)..f < (
N-min L~f)..f
proof
assume that
A1: f/.1 = W-max L~f and
A2: W-max L~f <> N-min L~f;
A3: N-min L~f in rng f by SPRECT_2:39;
then (N-min L~f)..f in dom f by FINSEQ_4:20;
then
A4: (N-min L~f)..f >= 1 by FINSEQ_3:25;
W-max L~f in rng f & (W-max L~f)..f = 1 by A1,FINSEQ_6:43,SPRECT_2:44;
hence thesis by A3,A2,A4,FINSEQ_5:9,XXREAL_0:1;
end;
theorem
z/.1 = W-max L~z implies (N-min L~z)..z < (N-max L~z)..z
proof
set g = Rotate(z,S-max L~z);
A1: L~z = L~g by REVROT_1:33;
S-max L~z in rng z by SPRECT_2:42;
then g/.1 = S-max L~g by A1,FINSEQ_6:92;
then
A2: (W-max L~g)..g <= (N-min L~g)..g & (N-min L~g)..g < (N-max L~g)..g by Th33
,Th34;
A3: N-min L~g in rng g by SPRECT_2:39;
assume
A4: z/.1 = W-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,W-max L~z) = z by A4,FINSEQ_6:181;
N-max L~g in rng g & W-max L~g in rng g by SPRECT_2:40,44;
hence thesis by A1,A5,A3,A2,Th5;
end;
theorem
z/.1 = W-max L~z & N-max L~z <> E-max L~z implies (N-max L~z)..z < (
E-max L~z)..z
proof
set g = Rotate(z,S-max L~z);
A1: L~z = L~g by REVROT_1:33;
S-max L~z in rng z by SPRECT_2:42;
then
A2: g/.1 = S-max L~g by A1,FINSEQ_6:92;
then
A3: E-max L~g in rng g & (W-max L~g)..g < (N-max L~g)..g by Lm23,SPRECT_2:46;
assume that
A4: z/.1 = W-max L~z and
A5: N-max L~z <> E-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,W-max L~z) = z by A4,FINSEQ_6:181;
A7: N-max L~g in rng g & W-max L~g in rng g by SPRECT_2:40,44;
(N-max L~g)..g < (E-max L~g)..g by A1,A5,A2,Th35;
hence thesis by A1,A6,A7,A3,Th5;
end;
theorem
z/.1 = W-max L~z implies (E-max L~z)..z < (E-min L~z)..z
proof
set g = Rotate(z,W-min L~z);
A1: L~z = L~g by REVROT_1:33;
W-min L~z in rng z by SPRECT_2:43;
then g/.1 = W-min L~g by A1,FINSEQ_6:92;
then
A2: (E-max L~g)..g < (E-min L~g)..g & (W-max L~g)..g < (E-max L~g)..g by Lm18
,Th26;
A3: W-max L~g in rng g by SPRECT_2:44;
assume
A4: z/.1 = W-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,W-max L~z) = z by A4,FINSEQ_6:181;
E-max L~g in rng g & E-min L~g in rng g by SPRECT_2:45,46;
hence thesis by A1,A5,A3,A2,Th5;
end;
theorem
z/.1 = W-max L~z & E-min L~z <> S-max L~z implies (E-min L~z)..z < (
S-max L~z)..z
proof
set g = Rotate(z,W-min L~z);
A1: L~z = L~g by REVROT_1:33;
W-min L~z in rng z by SPRECT_2:43;
then
A2: g/.1 = W-min L~g by A1,FINSEQ_6:92;
then
A3: (W-max L~g)..g < (E-min L~g)..g by Lm19;
assume that
A4: z/.1 = W-max L~z and
A5: E-min L~z <> S-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,W-max L~z) = z by A4,FINSEQ_6:181;
A7: S-max L~g in rng g & E-min L~g in rng g by SPRECT_2:42,45;
W-max L~g in rng g & (E-min L~g)..g < (S-max L~g)..g by A1,A5,A2,Th27,
SPRECT_2:44;
hence thesis by A1,A6,A7,A3,Th5;
end;
theorem
z/.1 = W-max L~z implies (S-max L~z)..z < (S-min L~z)..z
proof
set g = Rotate(z,E-max L~z);
A1: L~z = L~g by REVROT_1:33;
E-max L~z in rng z by SPRECT_2:46;
then g/.1 = E-max L~g by A1,FINSEQ_6:92;
then
A2: (S-max L~g)..g < (S-min L~g)..g & (S-min L~g)..g < (W-max L~g)..g by Lm30
,Th40;
A3: W-max L~g in rng g by SPRECT_2:44;
assume
A4: z/.1 = W-max L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A5: Rotate(g,W-max L~z) = z by A4,FINSEQ_6:181;
S-max L~g in rng g & S-min L~g in rng g by SPRECT_2:41,42;
hence thesis by A1,A5,A3,A2,Th11;
end;
theorem
z/.1 = W-max L~z & W-min L~z <> S-min L~z implies (S-min L~z)..z < (
W-min L~z)..z
proof
set g = Rotate(z,E-max L~z);
A1: L~z = L~g by REVROT_1:33;
E-max L~z in rng z by SPRECT_2:46;
then
A2: g/.1 = E-max L~g by A1,FINSEQ_6:92;
then
A3: (W-min L~g)..g < (W-max L~g)..g by Th42;
assume that
A4: z/.1 = W-max L~z and
A5: W-min L~z <> S-min L~z;
for i be Nat st 1 < i & i < len z holds z/.i <> z/.1 by
GOBOARD7:36;
then
A6: Rotate(g,W-max L~z) = z by A4,FINSEQ_6:181;
A7: W-min L~g in rng g & S-min L~g in rng g by SPRECT_2:41,43;
W-max L~g in rng g & (S-min L~g)..g < (W-min L~g)..g by A1,A5,A2,Th41,
SPRECT_2:44;
hence thesis by A1,A6,A7,A3,Th11;
end;