let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for x, p being Point of (TOP-REAL 2) st x in N-most C & p in (north_halfline x) /\ (L~ (Cage C,n)) holds
p `2 = N-bound (L~ (Cage C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for x, p being Point of (TOP-REAL 2) st x in N-most C & p in (north_halfline x) /\ (L~ (Cage C,n)) holds
p `2 = N-bound (L~ (Cage C,n))
let x, p be Point of (TOP-REAL 2); :: thesis: ( x in N-most C & p in (north_halfline x) /\ (L~ (Cage C,n)) implies p `2 = N-bound (L~ (Cage C,n)) )
set G = Gauge C,n;
set f = Cage C,n;
A1: Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
assume A2: x in N-most C ; :: thesis: ( not p in (north_halfline x) /\ (L~ (Cage C,n)) or p `2 = N-bound (L~ (Cage C,n)) )
then A3: x in C by XBOOLE_0:def 4;
assume A4: p in (north_halfline x) /\ (L~ (Cage C,n)) ; :: thesis: p `2 = N-bound (L~ (Cage C,n))
then p in L~ (Cage C,n) by XBOOLE_0:def 4;
then consider i being Element of NAT such that
A5: 1 <= i and
A6: i + 1 <= len (Cage C,n) and
A7: p in LSeg (Cage C,n),i by SPPOL_2:13;
A8: LSeg (Cage C,n),i = LSeg ((Cage C,n) /. i),((Cage C,n) /. (i + 1)) by A5, A6, TOPREAL1:def 5;
A9: i < len (Cage C,n) by A6, NAT_1:13;
then i in Seg (len (Cage C,n)) by A5, FINSEQ_1:3;
then i in dom (Cage C,n) by FINSEQ_1:def 3;
then consider i1, i2 being Element of NAT such that
A10: [i1,i2] in Indices (Gauge C,n) and
A11: (Cage C,n) /. i = (Gauge C,n) * i1,i2 by A1, GOBOARD1:def 11;
A12: 1 <= i2 by A10, MATRIX_1:39;
p in north_halfline x by A4, XBOOLE_0:def 4;
then LSeg (Cage C,n),i is horizontal by A2, A5, A7, A9, Th99;
then ((Cage C,n) /. i) `2 = ((Cage C,n) /. (i + 1)) `2 by A8, SPPOL_1:36;
then A13: p `2 = ((Cage C,n) /. i) `2 by A7, A8, GOBOARD7:6;
A14: i2 <= width (Gauge C,n) by A10, MATRIX_1:39;
A15: ( 1 <= i1 & i1 <= len (Gauge C,n) ) by A10, MATRIX_1:39;
A16: (len (Gauge C,n)) -' 1 <= len (Gauge C,n) by NAT_D:35;
A17: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
x `2 = (N-min C) `2 by A2, PSCOMP_1:98
.= N-bound C by EUCLID:56
.= ((Gauge C,n) * i1,((len (Gauge C,n)) -' 1)) `2 by A15, JORDAN8:17 ;
then i2 > (len (Gauge C,n)) -' 1 by A3, A4, A11, A17, A12, A15, A13, A16, Th95, SPRECT_3:24;
then i2 >= ((len (Gauge C,n)) -' 1) + 1 by NAT_1:13;
then i2 >= len (Gauge C,n) by A12, XREAL_1:237, XXREAL_0:2;
then i2 = len (Gauge C,n) by A17, A14, XXREAL_0:1;
then (Cage C,n) /. i in N-most (L~ (Cage C,n)) by A5, A9, A11, A17, A15, Th79;
hence p `2 = N-bound (L~ (Cage C,n)) by A13, Th11; :: thesis: verum