let j, i be Nat; :: thesis:
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
assume that
A1: C is connected and
A2: i <= j and
A3: not L~ (Cage (C,j)) c= Cl (RightComp (Cage (C,i))) ; :: thesis:
A4: Cage (C,j) is_sequence_on Gauge (C,j) by A1, JORDAN9:def 1;
A5: GoB (Cage (C,i)) = Gauge (C,i) by A1, Th44;
consider p being Point of (TOP-REAL 2) such that
A6: p in L~ (Cage (C,j)) and
A7: not p in Cl (RightComp (Cage (C,i))) by A3;
consider i1 being Nat such that
A8: 1 <= i1 and
A9: i1 + 1 <= len (Cage (C,j)) and
A10: p in LSeg ((Cage (C,j)),i1) by A6, SPPOL_2:13;
A11: GoB (Cage (C,j)) = Gauge (C,j) by A1, Th44;
then A12: right_cell ((Cage (C,j)),i1,(Gauge (C,j))) = right_cell ((Cage (C,j)),i1) by A8, A9, Th23;
A13: i1 < len (Cage (C,j)) by A9, NAT_1:13;

now :: thesis:

ex i2, j2 being Nat st
( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) )

proof

set f = Cage (C,j);
A14: i1 in dom (Cage (C,j)) by A8, A13, FINSEQ_3:25;
then consider i4, j4 being Nat such that
A15: [i4,j4] in Indices (Gauge (C,j)) and
A16: (Cage (C,j)) /. i1 = (Gauge (C,j)) * (i4,j4) by A4, GOBOARD1:def 9;
A17: 1 <= i4 by A15, MATRIX_0:32;
A18: j4 <= width (Gauge (C,j)) by A15, MATRIX_0:32;
A19: 1 <= j4 by A15, MATRIX_0:32;
A20: i4 <= len (Gauge (C,j)) by A15, MATRIX_0:32;
1 <= i1 + 1 by NAT_1:11;
then A21: i1 + 1 in dom (Cage (C,j)) by A9, FINSEQ_3:25;
then consider i5, j5 being Nat such that
A22: [i5,j5] in Indices (Gauge (C,j)) and
A23: (Cage (C,j)) /. (i1 + 1) = (Gauge (C,j)) * (i5,j5) by A4, GOBOARD1:def 9;
A24: 1 <= i5 by A22, MATRIX_0:32;
right_cell ((Cage (C,j)),i1) = right_cell ((Cage (C,j)),i1) ;
then A25: ( ( i4 = i5 & j4 + 1 = j5 & right_cell ((Cage (C,j)),i1) = cell ((GoB (Cage (C,j))),i4,j4) ) or ( i4 + 1 = i5 & j4 = j5 & right_cell ((Cage (C,j)),i1) = cell ((GoB (Cage (C,j))),i4,(j4 -' 1)) ) or ( i4 = i5 + 1 & j4 = j5 & right_cell ((Cage (C,j)),i1) = cell ((GoB (Cage (C,j))),i5,j5) ) or ( i4 = i5 & j4 = j5 + 1 & right_cell ((Cage (C,j)),i1) = cell ((GoB (Cage (C,j))),(i4 -' 1),j5) ) ) by A8, A9, A11, A15, A16, A22, A23, GOBOARD5:def 6;
|.(i4 - i5).| + |.(j4 - j5).| = 1 by A4, A14, A15, A16, A21, A22, A23, GOBOARD1:def 9;
then A26: ( ( |.(i4 - i5).| = 1 & j4 = j5 ) or ( |.(j4 - j5).| = 1 & i4 = i5 ) ) by SEQM_3:42;
A27: j5 <= width (Gauge (C,j)) by A22, MATRIX_0:32;
A28: i5 <= len (Gauge (C,j)) by A22, MATRIX_0:32;
A29: 1 <= j5 by A22, MATRIX_0:32;

per cases by A26, SEQM_3:41;

suppose A30: ( i4 = i5 & j4 + 1 = j5 ) ; :: thesis:

then i4 < len (Gauge (C,j)) by A1, A8, A9, A15, A16, A22, A23, JORDAN10:1;
then i4 + 1 <= len (Gauge (C,j)) by NAT_1:13;
hence ex i2, j2 being Nat st
( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A11, A17, A19, A27, A25, A30, Th38; :: thesis:

end;

suppose A31: ( i4 + 1 = i5 & j4 = j5 ) ; :: thesis:

then 1 < j4 by A1, A8, A9, A15, A16, A22, A23, JORDAN10:3;
then 1 + 1 <= j4 by NAT_1:13;
then A32: 1 <= j4 -' 1 by JORDAN5B:2;
(j4 -' 1) + 1 = j4 by A19, XREAL_1:235;
hence ex i2, j2 being Nat st
( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A11, A17, A18, A28, A25, A31, A32, Th38; :: thesis:

end;

suppose A33: ( i4 = i5 + 1 & j4 = j5 ) ; :: thesis:

then j5 < width (Gauge (C,j)) by A1, A8, A9, A15, A16, A22, A23, JORDAN10:4;
then j5 + 1 <= width (Gauge (C,j)) by NAT_1:13;
hence ex i2, j2 being Nat st
( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A11, A20, A24, A29, A25, A33, Th38; :: thesis:

end;

suppose A34: ( i4 = i5 & j4 = j5 + 1 ) ; :: thesis:

then 1 < i4 by A1, A8, A9, A15, A16, A22, A23, JORDAN10:2;
then 1 + 1 <= i4 by NAT_1:13;
then A35: 1 <= i4 -' 1 by JORDAN5B:2;
(i4 -' 1) + 1 = i4 by A17, XREAL_1:235;
hence ex i2, j2 being Nat st
( 1 <= i2 & i2 + 1 <= len (Gauge (C,i)) & 1 <= j2 & j2 + 1 <= width (Gauge (C,i)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ) by A2, A11, A20, A18, A29, A25, A34, A35, Th38; :: thesis:

end;

then consider i2, j2 being Nat such that
1 <= i2 and
A36: i2 + 1 <= len (Gauge (C,i)) and
1 <= j2 and
A37: j2 + 1 <= width (Gauge (C,i)) and
A38: right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) ;
A39: Int (right_cell ((Cage (C,j)),i1)) c= Int (cell ((Gauge (C,i)),i2,j2)) by A38, TOPS_1:19;
A40: RightComp (Cage (C,i)) is_a_component_of (L~ (Cage (C,i))) ` by GOBOARD9:def 2;
A41: (Cl (LeftComp (Cage (C,i)))) \/ (RightComp (Cage (C,i))) = ((L~ (Cage (C,i))) \/ (LeftComp (Cage (C,i)))) \/ (RightComp (Cage (C,i))) by GOBRD14:22
.= ((L~ (Cage (C,i))) \/ (RightComp (Cage (C,i)))) \/ (LeftComp (Cage (C,i))) by XBOOLE_1:4
.= the carrier of (TOP-REAL 2) by GOBRD14:15 ;
assume not right_cell ((Cage (C,j)),i1) c= Cl (LeftComp (Cage (C,i))) ; :: thesis:
then not cell ((Gauge (C,i)),i2,j2) c= Cl (LeftComp (Cage (C,i))) by A38;
then A42: cell ((Gauge (C,i)),i2,j2) meets RightComp (Cage (C,i)) by A41, XBOOLE_1:73;
A43: ( i2 < len (Gauge (C,i)) & j2 < width (Gauge (C,i)) ) by A36, A37, NAT_1:13;
then cell ((Gauge (C,i)),i2,j2) = Cl (Int (cell ((Gauge (C,i)),i2,j2))) by GOBRD11:35;
then A44: Int (cell ((Gauge (C,i)),i2,j2)) meets RightComp (Cage (C,i)) by A42, TSEP_1:36;
A45: Int (cell ((Gauge (C,i)),i2,j2)) is convex by A43, GOBOARD9:17;
Int (cell ((Gauge (C,i)),i2,j2)) c= (L~ (Cage (C,i))) ` by A5, A43, GOBRD12:1;
then Int (cell ((Gauge (C,i)),i2,j2)) c= RightComp (Cage (C,i)) by A44, A40, A45, GOBOARD9:4;
then Int (right_cell ((Cage (C,j)),i1)) c= RightComp (Cage (C,i)) by A39;
then Cl (Int (right_cell ((Cage (C,j)),i1))) c= Cl (RightComp (Cage (C,i))) by PRE_TOPC:19;
then A46: right_cell ((Cage (C,j)),i1) c= Cl (RightComp (Cage (C,i))) by A4, A8, A9, A12, JORDAN9:11;
( LSeg ((Cage (C,j)),i1) c= right_cell ((Cage (C,j)),i1,(Gauge (C,j))) & right_cell ((Cage (C,j)),i1,(Gauge (C,j))) c= right_cell ((Cage (C,j)),i1) ) by A4, A8, A9, Th22, GOBRD13:33;
then LSeg ((Cage (C,j)),i1) c= right_cell ((Cage (C,j)),i1) ;
then LSeg ((Cage (C,j)),i1) c= Cl (RightComp (Cage (C,i))) by A46;
hence contradiction by A7, A10; :: thesis:

end;

then A47: C meets Cl (LeftComp (Cage (C,i))) by A1, A8, A9, A12, JORDAN9:31, XBOOLE_1:63;
( Cl (LeftComp (Cage (C,i))) = (LeftComp (Cage (C,i))) \/ (L~ (Cage (C,i))) & C misses L~ (Cage (C,i)) ) by A1, GOBRD14:22, JORDAN10:5;
then A48: C meets LeftComp (Cage (C,i)) by A47, XBOOLE_1:70;
reconsider D = (L~ (Cage (C,i))) ` as Subset of (TOP-REAL 2) ;
D = (LeftComp (Cage (C,i))) \/ (RightComp (Cage (C,i))) by GOBRD12:10;
then A49: RightComp (Cage (C,i)) c= D by XBOOLE_1:7;
C c= RightComp (Cage (C,i)) by A1, JORDAN10:11;
then A50: C c= D by A49;
C meets C ;
then A51: C meets RightComp (Cage (C,i)) by A1, JORDAN10:11, XBOOLE_1:63;
( LeftComp (Cage (C,i)) is_a_component_of D & RightComp (Cage (C,i)) is_a_component_of D ) by GOBOARD9:def 1, GOBOARD9:def 2;
hence contradiction by A1, A48, A50, A51, JORDAN9:1, SPRECT_4:6; :: thesis: