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) * 1,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) * 1,t )
consider x being set such that
A1: x in W-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 ) } = west_halfline x by TOPREAL1:43;
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) * 1,t ; :: thesis: contradiction

A5: now

west_halfline x meets L~ (Cage C,n) by A2, Th75;
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: 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:11;
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;

A15: y in LSeg ((Cage C,n) /. i),((Cage C,n) /. (i + 1)) by A11, A12, A13, TOPREAL1:def 5;

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: x in UBD (L~ (Cage C,n))

then ((Cage C,n) /. i) `1 <= q `1 by A8, A15, TOPREAL1:9;
then A16: ((Cage C,n) /. i) `1 < x `1 by A14, XXREAL_0:2;
A17: Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
A18: i < len (Cage C,n) by A12, NAT_1:13;
then i in Seg (len (Cage C,n)) by A11, 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
A19: [i1,i2] in Indices (Gauge C,n) and
A20: (Cage C,n) /. i = (Gauge C,n) * i1,i2 by A17, GOBOARD1:def 11;
A21: 1 <= i2 by A19, MATRIX_1:39;
A22: i1 <= len (Gauge C,n) by A19, MATRIX_1:39;
A23: 1 <= i1 by A19, MATRIX_1:39;
A24: i2 <= width (Gauge C,n) by A19, MATRIX_1:39;
then A25: i2 <= len (Gauge C,n) by JORDAN8:def 1;
x `1 = (W-min C) `1 by A1, PSCOMP_1:88
.= W-bound C by EUCLID:56
.= ((Gauge C,n) * 2,i2) `1 by A21, A25, JORDAN8:14 ;
then i1 < 1 + 1 by A16, A20, A21, A24, A22, SPRECT_3:25;
then i1 <= 1 by NAT_1:13;
then (Cage C,n) /. i = (Gauge C,n) * 1,i2 by A20, A23, XXREAL_0:1;
hence x in UBD (L~ (Cage C,n)) by A4, A11, A18, A21, A24; :: thesis: verum

end;

suppose ((Cage C,n) /. i) `1 >= ((Cage C,n) /. (i + 1)) `1 ; :: thesis: x in UBD (L~ (Cage C,n))

then q `1 >= ((Cage C,n) /. (i + 1)) `1 by A8, A15, TOPREAL1:9;
then A26: ((Cage C,n) /. (i + 1)) `1 < x `1 by A14, XXREAL_0:2;
A27: Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
A28: i + 1 >= 1 by NAT_1:11;
then i + 1 in Seg (len (Cage C,n)) by A12, FINSEQ_1:3;
then i + 1 in dom (Cage C,n) by FINSEQ_1:def 3;
then consider i1, i2 being Element of NAT such that
A29: [i1,i2] in Indices (Gauge C,n) and
A30: (Cage C,n) /. (i + 1) = (Gauge C,n) * i1,i2 by A27, GOBOARD1:def 11;
A31: 1 <= i2 by A29, MATRIX_1:39;
A32: i1 <= len (Gauge C,n) by A29, MATRIX_1:39;
A33: 1 <= i1 by A29, MATRIX_1:39;
A34: i2 <= width (Gauge C,n) by A29, MATRIX_1:39;
then A35: i2 <= len (Gauge C,n) by JORDAN8:def 1;
x `1 = (W-min C) `1 by A1, PSCOMP_1:88
.= W-bound C by EUCLID:56
.= ((Gauge C,n) * 2,i2) `1 by A31, A35, JORDAN8:14 ;
then i1 < 1 + 1 by A26, A30, A31, A34, A32, SPRECT_3:25;
then i1 <= 1 by NAT_1:13;
then (Cage C,n) /. (i + 1) = (Gauge C,n) * 1,i2 by A30, A33, XXREAL_0:1;
hence x in UBD (L~ (Cage C,n)) by A4, A12, A28, A31, A34; :: 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:28; :: thesis: verum