let i, j be Element of 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, Th52;
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, SUBSET_1:7;
consider i1 being Element of 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, Th52;
then A12: right_cell ((Cage (C,j)),i1,(Gauge (C,j))) = right_cell ((Cage (C,j)),i1) by A8, A9, Th29;
A13: i1 < len (Cage (C,j)) by A9, NAT_1:13;

now

ex i2, j2 being Element of 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:27;
then consider i4, j4 being Element of 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 11;
A17: 1 <= i4 by A15, MATRIX_1:39;
A18: j4 <= width (Gauge (C,j)) by A15, MATRIX_1:39;
A19: 1 <= j4 by A15, MATRIX_1:39;
A20: i4 <= len (Gauge (C,j)) by A15, MATRIX_1:39;
1 <= i1 + 1 by NAT_1:11;
then A21: i1 + 1 in dom (Cage (C,j)) by A9, FINSEQ_3:27;
then consider i5, j5 being Element of 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 11;
A24: 1 <= i5 by A22, MATRIX_1:39;
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;
(abs (i4 - i5)) + (abs (j4 - j5)) = 1 by A4, A14, A15, A16, A21, A22, A23, GOBOARD1:def 11;
then A26: ( ( abs (i4 - i5) = 1 & j4 = j5 ) or ( abs (j4 - j5) = 1 & i4 = i5 ) ) by SEQM_3:82;
A27: j5 <= width (Gauge (C,j)) by A22, MATRIX_1:39;
A28: i5 <= len (Gauge (C,j)) by A22, MATRIX_1:39;
A29: 1 <= j5 by A22, MATRIX_1:39;

per cases by A26, SEQM_3:81;

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 Element of 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, Th44; :: 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:237;
hence ex i2, j2 being Element of 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, Th44; :: 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 Element of 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, Th44; :: 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:237;
hence ex i2, j2 being Element of 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, Th44; :: thesis:

end;

then consider i2, j2 being Element of 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:48;
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:32
.= ((L~ (Cage (C,i))) \/ (RightComp (Cage (C,i)))) \/ (LeftComp (Cage (C,i))) by XBOOLE_1:4
.= the carrier of (TOP-REAL 2) by GOBRD14:25 ;
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, XBOOLE_1:1;
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:40;
Int (cell ((Gauge (C,i)),i2,j2)) c= (L~ (Cage (C,i))) ` by A5, A43, GOBRD12:2;
then Int (cell ((Gauge (C,i)),i2,j2)) c= RightComp (Cage (C,i)) by A43, A44, A40, GOBOARD9:6, GOBOARD9:21;
then Int (right_cell ((Cage (C,j)),i1)) c= RightComp (Cage (C,i)) by A39, XBOOLE_1:1;
then Cl (Int (right_cell ((Cage (C,j)),i1))) c= Cl (RightComp (Cage (C,i))) by PRE_TOPC:49;
then A45: right_cell ((Cage (C,j)),i1) c= Cl (RightComp (Cage (C,i))) by A4, A8, A9, A12, JORDAN9:13;
( 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, Th28, GOBRD13:34;
then LSeg ((Cage (C,j)),i1) c= right_cell ((Cage (C,j)),i1) by XBOOLE_1:1;
then LSeg ((Cage (C,j)),i1) c= Cl (RightComp (Cage (C,i))) by A45, XBOOLE_1:1;
hence contradiction by A7, A10; :: thesis:

end;

then A46: C meets Cl (LeftComp (Cage (C,i))) by A1, A8, A9, A12, JORDAN9:33, 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:32, JORDAN10:5;
then A47: C meets LeftComp (Cage (C,i)) by A46, 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:11;
then A48: RightComp (Cage (C,i)) c= D by XBOOLE_1:7;
C c= RightComp (Cage (C,i)) by A1, JORDAN10:11;
then A49: C c= D by A48, XBOOLE_1:1;
C meets C ;
then A50: 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, A47, A49, A50, JORDAN9:3, SPRECT_4:7; :: thesis: