let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ (Upper_Seq C,n) & p `1 = E-bound (L~ (Cage C,n)) holds
p = E-max (L~ (Cage C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in L~ (Upper_Seq C,n) & p `1 = E-bound (L~ (Cage C,n)) holds
p = E-max (L~ (Cage C,n))
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ (Upper_Seq C,n) & p `1 = E-bound (L~ (Cage C,n)) implies p = E-max (L~ (Cage C,n)) )
set Ca = Cage C,n;
set US = Upper_Seq C,n;
set LS = Lower_Seq C,n;
set Wmin = W-min (L~ (Cage C,n));
set Smax = S-max (L~ (Cage C,n));
set Smin = S-min (L~ (Cage C,n));
set Emin = E-min (L~ (Cage C,n));
set Emax = E-max (L~ (Cage C,n));
set Wbo = W-bound (L~ (Cage C,n));
set Nbo = N-bound (L~ (Cage C,n));
set Ebo = E-bound (L~ (Cage C,n));
set Sbo = S-bound (L~ (Cage C,n));
set NE = NE-corner (L~ (Cage C,n));
assume that
A1: p in L~ (Upper_Seq C,n) and
A2: p `1 = E-bound (L~ (Cage C,n)) and
A3: p <> E-max (L~ (Cage C,n)) ; :: thesis: contradiction
A4: (Upper_Seq C,n) /. 1 = W-min (L~ (Cage C,n)) by JORDAN1F:5;
1 in dom (Upper_Seq C,n) by FINSEQ_5:6;
then A5: (Upper_Seq C,n) . 1 = W-min (L~ (Cage C,n)) by A4, PARTFUN1:def 8;
W-bound (L~ (Cage C,n)) <> E-bound (L~ (Cage C,n)) by SPRECT_1:33;
then p <> (Upper_Seq C,n) . 1 by A2, A5, EUCLID:56;
then reconsider g = R_Cut (Upper_Seq C,n),p as being_S-Seq FinSequence of (TOP-REAL 2) by A1, JORDAN3:70;
<*p*> is_in_the_area_of Cage C,n by A1, JORDAN1E:21, SPRECT_3:63;
then A6: g is_in_the_area_of Cage C,n by A1, JORDAN1E:21, SPRECT_3:69;
len g in dom g by FINSEQ_5:6;
then A7: g /. (len g) = g . (len g) by PARTFUN1:def 8
.= p by A1, JORDAN3:59 ;
(g /. 1) `1 = ((Upper_Seq C,n) /. 1) `1 by A1, SPRECT_3:39
.= (W-min (L~ (Cage C,n))) `1 by JORDAN1F:5
.= W-bound (L~ (Cage C,n)) by EUCLID:56 ;
then A8: g is_a_h.c._for Cage C,n by A2, A6, A7, SPRECT_2:def 2;
A9: (Lower_Seq C,n) /. 1 = E-max (L~ (Cage C,n)) by JORDAN1F:6;
1 in dom (Lower_Seq C,n) by FINSEQ_5:6;
then A10: (Lower_Seq C,n) . 1 = E-max (L~ (Cage C,n)) by A9, PARTFUN1:def 8;
len (Cage C,n) > 4 by GOBOARD7:36;
then A11: rng (Cage C,n) c= L~ (Cage C,n) by SPPOL_2:18, XXREAL_0:2;
now
per cases ( E-max (L~ (Cage C,n)) <> NE-corner (L~ (Cage C,n)) or E-max (L~ (Cage C,n)) = NE-corner (L~ (Cage C,n)) ) ;
suppose A12: E-max (L~ (Cage C,n)) <> NE-corner (L~ (Cage C,n)) ; :: thesis: contradiction
A13: not NE-corner (L~ (Cage C,n)) in rng (Cage C,n)
proof
A14: (NE-corner (L~ (Cage C,n))) `1 = E-bound (L~ (Cage C,n)) by EUCLID:56;
A15: (NE-corner (L~ (Cage C,n))) `2 = N-bound (L~ (Cage C,n)) by EUCLID:56;
then (NE-corner (L~ (Cage C,n))) `2 >= S-bound (L~ (Cage C,n)) by SPRECT_1:24;
then NE-corner (L~ (Cage C,n)) in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = E-bound (L~ (Cage C,n)) & p1 `2 <= N-bound (L~ (Cage C,n)) & p1 `2 >= S-bound (L~ (Cage C,n)) ) } by A14, A15;
then A16: NE-corner (L~ (Cage C,n)) in LSeg (SE-corner (L~ (Cage C,n))),(NE-corner (L~ (Cage C,n))) by SPRECT_1:25;
assume NE-corner (L~ (Cage C,n)) in rng (Cage C,n) ; :: thesis: contradiction
then NE-corner (L~ (Cage C,n)) in (LSeg (SE-corner (L~ (Cage C,n))),(NE-corner (L~ (Cage C,n)))) /\ (L~ (Cage C,n)) by A11, A16, XBOOLE_0:def 4;
then A17: (NE-corner (L~ (Cage C,n))) `2 <= (E-max (L~ (Cage C,n))) `2 by PSCOMP_1:108;
A18: (E-max (L~ (Cage C,n))) `1 = (NE-corner (L~ (Cage C,n))) `1 by PSCOMP_1:105;
(E-max (L~ (Cage C,n))) `2 <= (NE-corner (L~ (Cage C,n))) `2 by PSCOMP_1:107;
then (E-max (L~ (Cage C,n))) `2 = (NE-corner (L~ (Cage C,n))) `2 by A17, XXREAL_0:1;
hence contradiction by A12, A18, TOPREAL3:11; :: thesis: verum
end;
S-max (L~ (Cage C,n)) in rng (Lower_Seq C,n) by Th12;
then R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))) = mid (Lower_Seq C,n),1,((S-max (L~ (Cage C,n))) .. (Lower_Seq C,n)) by JORDAN1G:57;
then A19: rng (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n)))) c= rng (Lower_Seq C,n) by FINSEQ_6:125;
rng (Lower_Seq C,n) c= rng (Cage C,n) by JORDAN1G:47;
then rng (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n)))) c= rng (Cage C,n) by A19, XBOOLE_1:1;
then not NE-corner (L~ (Cage C,n)) in rng (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n)))) by A13;
then rng (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n)))) misses {(NE-corner (L~ (Cage C,n)))} by ZFMISC_1:56;
then rng (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n)))) misses rng <*(NE-corner (L~ (Cage C,n)))*> by FINSEQ_1:55;
then A20: rng (Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) misses rng <*(NE-corner (L~ (Cage C,n)))*> by FINSEQ_5:60;
set h = (Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) ^ <*(NE-corner (L~ (Cage C,n)))*>;
A21: <*(NE-corner (L~ (Cage C,n)))*> is one-to-one by FINSEQ_3:102;
A22: (((Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) ^ <*(NE-corner (L~ (Cage C,n)))*>) /. (len ((Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) ^ <*(NE-corner (L~ (Cage C,n)))*>))) `2 = (((Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) ^ <*(NE-corner (L~ (Cage C,n)))*>) /. ((len (Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n)))))) + 1)) `2 by FINSEQ_2:19
.= (NE-corner (L~ (Cage C,n))) `2 by FINSEQ_4:82
.= N-bound (L~ (Cage C,n)) by EUCLID:56 ;
E-min (L~ (Cage C,n)) in L~ (Cage C,n) by SPRECT_1:16;
then A23: S-bound (L~ (Cage C,n)) <= (E-min (L~ (Cage C,n))) `2 by PSCOMP_1:71;
A24: (Index (S-max (L~ (Cage C,n))),(Lower_Seq C,n)) + 1 >= 0 + 1 by XREAL_1:9;
A25: S-max (L~ (Cage C,n)) in L~ (Lower_Seq C,n) by Th12;
then <*(S-max (L~ (Cage C,n)))*> is_in_the_area_of Cage C,n by JORDAN1E:22, SPRECT_3:63;
then R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))) is_in_the_area_of Cage C,n by A25, JORDAN1E:22, SPRECT_3:69;
then A26: Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n)))) is_in_the_area_of Cage C,n by SPRECT_3:68;
(E-min (L~ (Cage C,n))) `2 < (E-max (L~ (Cage C,n))) `2 by SPRECT_2:57;
then A27: S-max (L~ (Cage C,n)) <> (Lower_Seq C,n) . 1 by A10, A23, EUCLID:56;
then reconsider RCutLS = R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))) as being_S-Seq FinSequence of (TOP-REAL 2) by A25, JORDAN3:70;
A28: Rev RCutLS is special by SPPOL_2:42;
len ((Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) ^ <*(NE-corner (L~ (Cage C,n)))*>) = (len (Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n)))))) + 1 by FINSEQ_2:19
.= (len (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) + 1 by FINSEQ_5:def 3
.= ((Index (S-max (L~ (Cage C,n))),(Lower_Seq C,n)) + 1) + 1 by A25, A27, JORDAN3:60 ;
then A29: len ((Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) ^ <*(NE-corner (L~ (Cage C,n)))*>) >= 1 + 1 by A24, XREAL_1:9;
A30: 2 <= len g by TOPREAL1:def 10;
A31: <*(NE-corner (L~ (Cage C,n)))*> is special ;
1 in dom (Rev RCutLS) by FINSEQ_5:6;
then ((Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) ^ <*(NE-corner (L~ (Cage C,n)))*>) /. 1 = (Rev RCutLS) /. 1 by FINSEQ_4:83
.= (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n)))) /. (len (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) by FINSEQ_5:68
.= S-max (L~ (Cage C,n)) by A25, Th45 ;
then A32: (((Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) ^ <*(NE-corner (L~ (Cage C,n)))*>) /. 1) `2 = S-bound (L~ (Cage C,n)) by EUCLID:56;
<*(NE-corner (L~ (Cage C,n)))*> is_in_the_area_of Cage C,n by SPRECT_2:29;
then (Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) ^ <*(NE-corner (L~ (Cage C,n)))*> is_in_the_area_of Cage C,n by A26, SPRECT_2:28;
then A33: (Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) ^ <*(NE-corner (L~ (Cage C,n)))*> is_a_v.c._for Cage C,n by A32, A22, SPRECT_2:def 3;
A34: len (Lower_Seq C,n) in dom (Lower_Seq C,n) by FINSEQ_5:6;
A35: (Rev RCutLS) /. (len (Rev RCutLS)) = (Rev RCutLS) /. (len RCutLS) by FINSEQ_5:def 3
.= RCutLS /. 1 by FINSEQ_5:68
.= (Lower_Seq C,n) /. 1 by A25, SPRECT_3:39
.= E-max (L~ (Cage C,n)) by JORDAN1F:6 ;
then ((Rev RCutLS) /. (len (Rev RCutLS))) `1 = E-bound (L~ (Cage C,n)) by EUCLID:56
.= (NE-corner (L~ (Cage C,n))) `1 by EUCLID:56
.= (<*(NE-corner (L~ (Cage C,n)))*> /. 1) `1 by FINSEQ_4:25 ;
then ( (Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) ^ <*(NE-corner (L~ (Cage C,n)))*> is one-to-one & (Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) ^ <*(NE-corner (L~ (Cage C,n)))*> is special ) by A20, A21, A28, A31, FINSEQ_3:98, GOBOARD2:13;
then L~ g meets L~ ((Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) ^ <*(NE-corner (L~ (Cage C,n)))*>) by A8, A30, A29, A33, SPRECT_2:33;
then consider x being set such that
A36: x in L~ g and
A37: x in L~ ((Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) ^ <*(NE-corner (L~ (Cage C,n)))*>) by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A36;
A38: L~ ((Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) ^ <*(NE-corner (L~ (Cage C,n)))*>) = (L~ (Rev RCutLS)) \/ (LSeg ((Rev RCutLS) /. (len (Rev RCutLS))),(NE-corner (L~ (Cage C,n)))) by SPPOL_2:19;
A39: L~ RCutLS c= L~ (Lower_Seq C,n) by Th12, JORDAN3:76;
A40: len (Upper_Seq C,n) in dom (Upper_Seq C,n) by FINSEQ_5:6;
A41: L~ g c= L~ (Upper_Seq C,n) by A1, JORDAN3:76;
then A42: x in L~ (Upper_Seq C,n) by A36;
now
per cases ( x in L~ (Rev RCutLS) or x in LSeg ((Rev RCutLS) /. (len (Rev RCutLS))),(NE-corner (L~ (Cage C,n))) ) by A37, A38, XBOOLE_0:def 3;
suppose x in L~ (Rev RCutLS) ; :: thesis: contradiction
then A43: x in L~ RCutLS by SPPOL_2:22;
then x in (L~ (Upper_Seq C,n)) /\ (L~ (Lower_Seq C,n)) by A36, A41, A39, XBOOLE_0:def 4;
then A44: x in {(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} by JORDAN1E:20;
now
per cases ( x = W-min (L~ (Cage C,n)) or x = E-max (L~ (Cage C,n)) ) by A44, TARSKI:def 2;
suppose x = W-min (L~ (Cage C,n)) ; :: thesis: contradiction
then (Lower_Seq C,n) /. (len (Lower_Seq C,n)) in L~ (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n)))) by A43, JORDAN1F:8;
then (Lower_Seq C,n) . (len (Lower_Seq C,n)) in L~ (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n)))) by A34, PARTFUN1:def 8;
then (Lower_Seq C,n) . (len (Lower_Seq C,n)) = S-max (L~ (Cage C,n)) by A25, Th43;
then (Lower_Seq C,n) /. (len (Lower_Seq C,n)) = S-max (L~ (Cage C,n)) by A34, PARTFUN1:def 8;
then A45: W-min (L~ (Cage C,n)) = S-max (L~ (Cage C,n)) by JORDAN1F:8;
S-min (L~ (Cage C,n)) in L~ (Cage C,n) by SPRECT_1:14;
then A46: W-bound (L~ (Cage C,n)) <= (S-min (L~ (Cage C,n))) `1 by PSCOMP_1:71;
(S-min (L~ (Cage C,n))) `1 < (S-max (L~ (Cage C,n))) `1 by SPRECT_2:59;
hence contradiction by A45, A46, EUCLID:56; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose A47: x in LSeg ((Rev RCutLS) /. (len (Rev RCutLS))),(NE-corner (L~ (Cage C,n))) ; :: thesis: contradiction
(E-max (L~ (Cage C,n))) `2 <= (NE-corner (L~ (Cage C,n))) `2 by PSCOMP_1:107;
then A48: (E-max (L~ (Cage C,n))) `2 <= x `2 by A35, A47, TOPREAL1:10;
A49: (E-max (L~ (Cage C,n))) `1 = E-bound (L~ (Cage C,n)) by EUCLID:56;
(NE-corner (L~ (Cage C,n))) `1 = E-bound (L~ (Cage C,n)) by EUCLID:56;
then A50: x `1 = E-bound (L~ (Cage C,n)) by A35, A47, A49, GOBOARD7:5;
L~ (Cage C,n) = (L~ (Upper_Seq C,n)) \/ (L~ (Lower_Seq C,n)) by JORDAN1E:17;
then L~ (Upper_Seq C,n) c= L~ (Cage C,n) by XBOOLE_1:7;
then x in E-most (L~ (Cage C,n)) by A42, A50, SPRECT_2:17;
then x `2 <= (E-max (L~ (Cage C,n))) `2 by PSCOMP_1:108;
then x `2 = (E-max (L~ (Cage C,n))) `2 by A48, XXREAL_0:1;
then x = E-max (L~ (Cage C,n)) by A49, A50, TOPREAL3:11;
then (Upper_Seq C,n) /. (len (Upper_Seq C,n)) in L~ (R_Cut (Upper_Seq C,n),p) by A36, JORDAN1F:7;
then (Upper_Seq C,n) . (len (Upper_Seq C,n)) in L~ (R_Cut (Upper_Seq C,n),p) by A40, PARTFUN1:def 8;
then (Upper_Seq C,n) . (len (Upper_Seq C,n)) = p by A1, Th43;
then (Upper_Seq C,n) /. (len (Upper_Seq C,n)) = p by A40, PARTFUN1:def 8;
hence contradiction by A3, JORDAN1F:7; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose A51: E-max (L~ (Cage C,n)) = NE-corner (L~ (Cage C,n)) ; :: thesis: contradiction
E-min (L~ (Cage C,n)) in L~ (Cage C,n) by SPRECT_1:16;
then A52: S-bound (L~ (Cage C,n)) <= (E-min (L~ (Cage C,n))) `2 by PSCOMP_1:71;
set h = Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))));
A53: 2 <= len g by TOPREAL1:def 10;
A54: S-max (L~ (Cage C,n)) in L~ (Lower_Seq C,n) by Th12;
then <*(S-max (L~ (Cage C,n)))*> is_in_the_area_of Cage C,n by JORDAN1E:22, SPRECT_3:63;
then R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))) is_in_the_area_of Cage C,n by A54, JORDAN1E:22, SPRECT_3:69;
then A55: Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n)))) is_in_the_area_of Cage C,n by SPRECT_3:68;
(E-min (L~ (Cage C,n))) `2 < (E-max (L~ (Cage C,n))) `2 by SPRECT_2:57;
then S-max (L~ (Cage C,n)) <> (Lower_Seq C,n) . 1 by A10, A52, EUCLID:56;
then reconsider RCutLS = R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))) as being_S-Seq FinSequence of (TOP-REAL 2) by A54, JORDAN3:70;
1 in dom (Rev RCutLS) by FINSEQ_5:6;
then (Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) /. 1 = (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n)))) /. (len (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) by FINSEQ_5:68
.= S-max (L~ (Cage C,n)) by A54, Th45 ;
then A56: ((Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) /. 1) `2 = S-bound (L~ (Cage C,n)) by EUCLID:56;
A57: Rev RCutLS is special by SPPOL_2:42;
len RCutLS >= 2 by TOPREAL1:def 10;
then A58: len (Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) >= 2 by FINSEQ_5:def 3;
(Rev RCutLS) /. (len (Rev RCutLS)) = (Rev RCutLS) /. (len RCutLS) by FINSEQ_5:def 3
.= RCutLS /. 1 by FINSEQ_5:68
.= (Lower_Seq C,n) /. 1 by A54, SPRECT_3:39
.= E-max (L~ (Cage C,n)) by JORDAN1F:6 ;
then ((Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) /. (len (Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))))) `2 = N-bound (L~ (Cage C,n)) by A51, EUCLID:56;
then Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n)))) is_a_v.c._for Cage C,n by A55, A56, SPRECT_2:def 3;
then L~ g meets L~ (Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) by A8, A57, A53, A58, SPRECT_2:33;
then consider x being set such that
A59: x in L~ g and
A60: x in L~ (Rev (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n))))) by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A59;
A61: x in L~ RCutLS by A60, SPPOL_2:22;
A62: L~ g c= L~ (Upper_Seq C,n) by A1, JORDAN3:76;
A63: len (Upper_Seq C,n) in dom (Upper_Seq C,n) by FINSEQ_5:6;
A64: len (Lower_Seq C,n) in dom (Lower_Seq C,n) by FINSEQ_5:6;
L~ RCutLS c= L~ (Lower_Seq C,n) by Th12, JORDAN3:76;
then x in (L~ (Upper_Seq C,n)) /\ (L~ (Lower_Seq C,n)) by A59, A62, A61, XBOOLE_0:def 4;
then A65: x in {(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} by JORDAN1E:20;
now
per cases ( x = W-min (L~ (Cage C,n)) or x = E-max (L~ (Cage C,n)) ) by A65, TARSKI:def 2;
suppose x = W-min (L~ (Cage C,n)) ; :: thesis: contradiction
then (Lower_Seq C,n) /. (len (Lower_Seq C,n)) in L~ (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n)))) by A61, JORDAN1F:8;
then (Lower_Seq C,n) . (len (Lower_Seq C,n)) in L~ (R_Cut (Lower_Seq C,n),(S-max (L~ (Cage C,n)))) by A64, PARTFUN1:def 8;
then (Lower_Seq C,n) . (len (Lower_Seq C,n)) = S-max (L~ (Cage C,n)) by A54, Th43;
then (Lower_Seq C,n) /. (len (Lower_Seq C,n)) = S-max (L~ (Cage C,n)) by A64, PARTFUN1:def 8;
then A66: W-min (L~ (Cage C,n)) = S-max (L~ (Cage C,n)) by JORDAN1F:8;
S-min (L~ (Cage C,n)) in L~ (Cage C,n) by SPRECT_1:14;
then A67: W-bound (L~ (Cage C,n)) <= (S-min (L~ (Cage C,n))) `1 by PSCOMP_1:71;
(S-min (L~ (Cage C,n))) `1 < (S-max (L~ (Cage C,n))) `1 by SPRECT_2:59;
hence contradiction by A66, A67, EUCLID:56; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum