let n be Nat; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for p, x 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); for p, x 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 p, x be Point of (TOP-REAL 2); ( 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
; ( 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)))
; p `2 = N-bound (L~ (Cage (C,n)))
then
p in L~ (Cage (C,n))
by XBOOLE_0:def 4;
then consider i being 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 3;
A9:
i < len (Cage (C,n))
by A6, NAT_1:13;
then
i in Seg (len (Cage (C,n)))
by A5, FINSEQ_1:1;
then
i in dom (Cage (C,n))
by FINSEQ_1:def 3;
then consider i1, i2 being 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 9;
A12:
1 <= i2
by A10, MATRIX_0:32;
p in north_halfline x
by A4, XBOOLE_0:def 4;
then
LSeg ((Cage (C,n)),i) is horizontal
by A2, A5, A7, A9, Th78;
then
((Cage (C,n)) /. i) `2 = ((Cage (C,n)) /. (i + 1)) `2
by A8, SPPOL_1:15;
then A13:
p `2 = ((Cage (C,n)) /. i) `2
by A7, A8, GOBOARD7:6;
A14:
i2 <= width (Gauge (C,n))
by A10, MATRIX_0:32;
A15:
( 1 <= i1 & i1 <= len (Gauge (C,n)) )
by A10, MATRIX_0:32;
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:39
.=
N-bound C
by EUCLID:52
.=
((Gauge (C,n)) * (i1,((len (Gauge (C,n))) -' 1))) `2
by A15, JORDAN8:14
;
then
i2 > (len (Gauge (C,n))) -' 1
by A3, A4, A11, A17, A12, A15, A13, A16, Th74, SPRECT_3:12;
then
i2 >= ((len (Gauge (C,n))) -' 1) + 1
by NAT_1:13;
then
i2 >= len (Gauge (C,n))
by A12, XREAL_1:235, 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, Th58;
hence
p `2 = N-bound (L~ (Cage (C,n)))
by A13, Th3; verum