let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Element of NAT st
( 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((len (Gauge (C,n))),t) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ex k, t being Element of NAT st
( 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((len (Gauge (C,n))),t) )
consider x being set such that
A1: x in E-most C by XBOOLE_0:def 1;
reconsider x = x as Point of (TOP-REAL 2) by A1;
A2: x in C by A1, XBOOLE_0:def 4;
set X = { q where q is Point of (TOP-REAL 2) : ( q `1 >= x `1 & q `2 = x `2 ) } ;
A3: { q where q is Point of (TOP-REAL 2) : ( q `1 >= x `1 & q `2 = x `2 ) } = east_halfline x by TOPREAL1:32;
then reconsider X = { q where q is Point of (TOP-REAL 2) : ( q `1 >= x `1 & q `2 = x `2 ) } as connected Subset of (TOP-REAL 2) ;
assume A4: for k, t being Element of NAT st 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) holds
(Cage (C,n)) /. k <> (Gauge (C,n)) * ((len (Gauge (C,n))),t) ; :: thesis: contradiction

A5: now

east_halfline x meets L~ (Cage (C,n)) by A2, Th73;
then consider y being set such that
A6: y in X and
A7: y in L~ (Cage (C,n)) by A3, XBOOLE_0:3;
reconsider y = y as Point of (TOP-REAL 2) by A6;
consider q being Point of (TOP-REAL 2) such that
A8: y = q and
A9: q `1 >= x `1 and
A10: q `2 = x `2 by A6;
consider i being Element of NAT such that
A11: 1 <= i and
A12: i + 1 <= len (Cage (C,n)) and
A13: y in LSeg ((Cage (C,n)),i) by A7, SPPOL_2:13;
A14: y in LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A11, A12, A13, TOPREAL1:def 3;
A15: q `1 > x `1

proof

assume q `1 <= x `1 ; :: thesis: contradiction
then q `1 = x `1 by A9, XXREAL_0:1;
then q = x by A10, TOPREAL3:6;
then x in C /\ (L~ (Cage (C,n))) by A2, A7, A8, XBOOLE_0:def 4;
then C meets L~ (Cage (C,n)) by XBOOLE_0:4;
hence contradiction by JORDAN10:5; :: thesis: verum

end;

A16: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
A17: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
A18: 4 <= len (Gauge (C,n)) by JORDAN8:10;
A19: 1 <= i + 1 by A11, NAT_1:13;
then i + 1 in Seg (len (Cage (C,n))) by A12, FINSEQ_1:1;
then i + 1 in dom (Cage (C,n)) by FINSEQ_1:def 3;
then consider l1, l2 being Element of NAT such that
A20: [l1,l2] in Indices (Gauge (C,n)) and
A21: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (l1,l2) by A16, GOBOARD1:def 9;
A22: 1 <= l2 by A20, MATRIX_1:38;
A23: l2 <= width (Gauge (C,n)) by A20, MATRIX_1:38;
then A24: l2 <= len (Gauge (C,n)) by JORDAN8:def 1;
A25: x `1 = (E-min C) `1 by A1, PSCOMP_1:47
.= E-bound C by EUCLID:52
.= ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),l2)) `1 by A22, A24, JORDAN8:12 ;
A26: l1 <= len (Gauge (C,n)) by A20, MATRIX_1:38;
A27: 1 <= l1 by A20, MATRIX_1:38;
A28: (len (Gauge (C,n))) -' 1 <= len (Gauge (C,n)) by NAT_D:35;
A29: i < len (Cage (C,n)) by A12, NAT_1:13;
then i in Seg (len (Cage (C,n))) by A11, FINSEQ_1:1;
then i in dom (Cage (C,n)) by FINSEQ_1:def 3;
then consider i1, i2 being Element of NAT such that
A30: [i1,i2] in Indices (Gauge (C,n)) and
A31: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,i2) by A17, GOBOARD1:def 9;
A32: 1 <= i2 by A30, MATRIX_1:38;
A33: i1 <= len (Gauge (C,n)) by A30, MATRIX_1:38;
A34: 1 <= i1 by A30, MATRIX_1:38;
A35: i2 <= width (Gauge (C,n)) by A30, MATRIX_1:38;
then A36: i2 <= len (Gauge (C,n)) by JORDAN8:def 1;
A37: x `1 = (E-min C) `1 by A1, PSCOMP_1:47
.= E-bound C by EUCLID:52
.= ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),i2)) `1 by A32, A36, JORDAN8:12 ;

now

per cases ( ((Cage (C,n)) /. i) `1 >= ((Cage (C,n)) /. (i + 1)) `1 or ((Cage (C,n)) /. i) `1 <= ((Cage (C,n)) /. (i + 1)) `1 ) ;

suppose ((Cage (C,n)) /. i) `1 >= ((Cage (C,n)) /. (i + 1)) `1 ; :: thesis: contradiction

then ((Cage (C,n)) /. i) `1 >= q `1 by A8, A14, TOPREAL1:3;
then ((Cage (C,n)) /. i) `1 > x `1 by A15, XXREAL_0:2;
then i1 > (len (Gauge (C,n))) -' 1 by A31, A32, A35, A34, A37, A28, SPRECT_3:13;
then i1 >= ((len (Gauge (C,n))) -' 1) + 1 by NAT_1:13;
then i1 >= len (Gauge (C,n)) by A18, XREAL_1:235, XXREAL_0:2;
then (Cage (C,n)) /. i = (Gauge (C,n)) * ((len (Gauge (C,n))),i2) by A31, A33, XXREAL_0:1;
hence contradiction by A4, A11, A29, A32, A35; :: thesis: verum

end;

suppose ((Cage (C,n)) /. i) `1 <= ((Cage (C,n)) /. (i + 1)) `1 ; :: thesis: contradiction

then q `1 <= ((Cage (C,n)) /. (i + 1)) `1 by A8, A14, TOPREAL1:3;
then ((Cage (C,n)) /. (i + 1)) `1 > x `1 by A15, XXREAL_0:2;
then l1 > (len (Gauge (C,n))) -' 1 by A21, A22, A23, A27, A25, A28, SPRECT_3:13;
then l1 >= ((len (Gauge (C,n))) -' 1) + 1 by NAT_1:13;
then l1 >= len (Gauge (C,n)) by A18, XREAL_1:235, XXREAL_0:2;
then (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * ((len (Gauge (C,n))),l2) by A21, A26, XXREAL_0:1;
hence contradiction by A4, A12, A19, A22, A23; :: thesis: verum

end;

end;

end;

hence x in UBD (L~ (Cage (C,n))) ; :: thesis: verum

end;

C c= BDD (L~ (Cage (C,n))) by JORDAN10:12;
then x in (BDD (L~ (Cage (C,n)))) /\ (UBD (L~ (Cage (C,n)))) by A2, A5, XBOOLE_0:def 4;
then BDD (L~ (Cage (C,n))) meets UBD (L~ (Cage (C,n))) by XBOOLE_0:4;
hence contradiction by JORDAN2C:24; :: thesis: verum