let n be Nat; :: thesis: 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 E-most C & p in (east_halfline x) /\ (L~ (Cage (C,n))) holds
p `1 = E-bound (L~ (Cage (C,n)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for p, x being Point of (TOP-REAL 2) st x in E-most C & p in (east_halfline x) /\ (L~ (Cage (C,n))) holds
p `1 = E-bound (L~ (Cage (C,n)))
let p, x be Point of (TOP-REAL 2); :: thesis: ( x in E-most C & p in (east_halfline x) /\ (L~ (Cage (C,n))) implies p `1 = E-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 E-most C ; :: thesis: ( not p in (east_halfline x) /\ (L~ (Cage (C,n))) or p `1 = E-bound (L~ (Cage (C,n))) )
then A3: x in C by XBOOLE_0:def 4;
A4: (len (Gauge (C,n))) -' 1 <= len (Gauge (C,n)) by NAT_D:35;
A5: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
assume A6: p in (east_halfline x) /\ (L~ (Cage (C,n))) ; :: thesis: p `1 = E-bound (L~ (Cage (C,n)))
then p in L~ (Cage (C,n)) by XBOOLE_0:def 4;
then consider i being Nat such that
A7: 1 <= i and
A8: i + 1 <= len (Cage (C,n)) and
A9: p in LSeg ((Cage (C,n)),i) by SPPOL_2:13;
A10: LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A7, A8, TOPREAL1:def 3;
A11: i < len (Cage (C,n)) by A8, NAT_1:13;
then i in Seg (len (Cage (C,n))) by A7, FINSEQ_1:1;
then i in dom (Cage (C,n)) by FINSEQ_1:def 3;
then consider i1, i2 being Nat such that
A12: [i1,i2] in Indices (Gauge (C,n)) and
A13: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,i2) by A1, GOBOARD1:def 9;
A14: ( 1 <= i2 & i2 <= width (Gauge (C,n)) ) by A12, MATRIX_0:32;
p in east_halfline x by A6, XBOOLE_0:def 4;
then LSeg ((Cage (C,n)),i) is vertical by A2, A7, A9, A11, Th79;
then ((Cage (C,n)) /. i) `1 = ((Cage (C,n)) /. (i + 1)) `1 by A10, SPPOL_1:16;
then A15: p `1 = ((Cage (C,n)) /. i) `1 by A9, A10, GOBOARD7:5;
A16: i1 <= len (Gauge (C,n)) by A12, MATRIX_0:32;
A17: 1 <= i1 by A12, MATRIX_0:32;
x `1 = (E-min C) `1 by A2, PSCOMP_1:47
.= E-bound C by EUCLID:52
.= ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),i2)) `1 by A5, A14, JORDAN8:12 ;
then i1 > (len (Gauge (C,n))) -' 1 by A3, A6, A13, A14, A17, A15, A4, Th75, SPRECT_3:13;
then i1 >= ((len (Gauge (C,n))) -' 1) + 1 by NAT_1:13;
then i1 >= len (Gauge (C,n)) by A17, XREAL_1:235, XXREAL_0:2;
then i1 = len (Gauge (C,n)) by A16, XXREAL_0:1;
then (Cage (C,n)) /. i in E-most (L~ (Cage (C,n))) by A7, A11, A13, A14, Th61;
hence p `1 = E-bound (L~ (Cage (C,n))) by A15, Th4; :: thesis: verum