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;
consider p being Point of (TOP-REAL 2) such that
A5: p in L~ (Cage C,j) and
A6: not p in Cl (RightComp (Cage C,i)) by A3, SUBSET_1:7;
reconsider D = (L~ (Cage C,i)) ` as Subset of (TOP-REAL 2) ;
consider i1 being Element of NAT such that
A7: 1 <= i1 and
A8: i1 + 1 <= len (Cage C,j) and
A9: p in LSeg (Cage C,j),i1 by A5, SPPOL_2:13;
A10: i1 < len (Cage C,j) by A8, NAT_1:13;
A11: GoB (Cage C,i) = Gauge C,i by A1, Th52;
A12: GoB (Cage C,j) = Gauge C,j by A1, Th52;
then A13: right_cell (Cage C,j),i1,(Gauge C,j) = right_cell (Cage C,j),i1 by A7, A8, Th29;

A14: now

assume A15: not right_cell (Cage C,j),i1 c= Cl (LeftComp (Cage C,i)) ; :: thesis:
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;
A16: i1 in dom (Cage C,j) by A7, A10, FINSEQ_3:27;
then consider i4, j4 being Element of NAT such that
A17: [i4,j4] in Indices (Gauge C,j) and
A18: (Cage C,j) /. i1 = (Gauge C,j) * i4,j4 by A4, GOBOARD1:def 11;
A19: ( 1 <= i4 & i4 <= len (Gauge C,j) ) by A17, MATRIX_1:39;
A20: ( 1 <= j4 & j4 <= width (Gauge C,j) ) by A17, MATRIX_1:39;
1 <= i1 + 1 by NAT_1:11;
then A21: i1 + 1 in dom (Cage C,j) by A8, 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 & i5 <= len (Gauge C,j) ) by A22, MATRIX_1:39;
A25: ( 1 <= j5 & j5 <= width (Gauge C,j) ) by A22, MATRIX_1:39;
right_cell (Cage C,j),i1 = right_cell (Cage C,j),i1 ;
then A26: ( ( 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 A7, A8, A12, A17, A18, A22, A23, GOBOARD5:def 6;
(abs (i4 - i5)) + (abs (j4 - j5)) = 1 by A4, A16, A17, A18, A21, A22, A23, GOBOARD1:def 11;
then A27: ( ( abs (i4 - i5) = 1 & j4 = j5 ) or ( abs (j4 - j5) = 1 & i4 = i5 ) ) by GOBOARD1:2;

per cases by A27, GOBOARD1:1;

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

then i4 < len (Gauge C,j) by A1, A7, A8, A17, A18, 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, A12, A19, A20, A25, A26, A28, Th44; :: thesis:

end;

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

A30: (j4 -' 1) + 1 = j4 by A20, XREAL_1:237;
1 < j4 by A1, A7, A8, A17, A18, A22, A23, A29, JORDAN10:3;
then 1 + 1 <= j4 by NAT_1:13;
then 1 <= j4 -' 1 by JORDAN5B:2;
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, A12, A19, A20, A24, A26, A29, A30, Th44; :: thesis:

end;

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

then j5 < width (Gauge C,j) by A1, A7, A8, A17, A18, 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, A12, A19, A24, A25, A26, A31, Th44; :: thesis:

end;

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

A33: (i4 -' 1) + 1 = i4 by A19, XREAL_1:237;
1 < i4 by A1, A7, A8, A17, A18, A22, A23, A32, JORDAN10:2;
then 1 + 1 <= i4 by NAT_1:13;
then 1 <= i4 -' 1 by JORDAN5B:2;
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, A12, A19, A20, A25, A26, A32, A33, Th44; :: thesis:

end;

then consider i2, j2 being Element of NAT such that
A34: ( 1 <= i2 & i2 + 1 <= len (Gauge C,i) ) and
A35: ( 1 <= j2 & j2 + 1 <= width (Gauge C,i) ) and
A36: right_cell (Cage C,j),i1 c= cell (Gauge C,i),i2,j2 ;
A37: i2 < len (Gauge C,i) by A34, NAT_1:13;
A38: j2 < width (Gauge C,i) by A35, NAT_1:13;
A39: not cell (Gauge C,i),i2,j2 c= Cl (LeftComp (Cage C,i)) by A15, A36, XBOOLE_1:1;
(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 ;
then A40: cell (Gauge C,i),i2,j2 meets RightComp (Cage C,i) by A39, XBOOLE_1:73;
cell (Gauge C,i),i2,j2 = Cl (Int (cell (Gauge C,i),i2,j2)) by A37, A38, GOBRD11:35;
then A41: Int (cell (Gauge C,i),i2,j2) meets RightComp (Cage C,i) by A40, TSEP_1:40;
A42: Int (cell (Gauge C,i),i2,j2) c= (L~ (Cage C,i)) ` by A11, A37, A38, GOBRD12:2;
RightComp (Cage C,i) is_a_component_of (L~ (Cage C,i)) ` by GOBOARD9:def 2;
then A43: Int (cell (Gauge C,i),i2,j2) c= RightComp (Cage C,i) by A37, A38, A41, A42, GOBOARD9:6, GOBOARD9:21;
Int (right_cell (Cage C,j),i1) c= Int (cell (Gauge C,i),i2,j2) by A36, TOPS_1:48;
then Int (right_cell (Cage C,j),i1) c= RightComp (Cage C,i) by A43, XBOOLE_1:1;
then Cl (Int (right_cell (Cage C,j),i1)) c= Cl (RightComp (Cage C,i)) by PRE_TOPC:49;
then A44: right_cell (Cage C,j),i1 c= Cl (RightComp (Cage C,i)) by A4, A7, A8, A13, JORDAN9:13;
A45: LSeg (Cage C,j),i1 c= right_cell (Cage C,j),i1,(Gauge C,j) by A4, A7, A8, Th28;
right_cell (Cage C,j),i1,(Gauge C,j) c= right_cell (Cage C,j),i1 by A4, A7, A8, GOBRD13:34;
then LSeg (Cage C,j),i1 c= right_cell (Cage C,j),i1 by A45, XBOOLE_1:1;
then LSeg (Cage C,j),i1 c= Cl (RightComp (Cage C,i)) by A44, XBOOLE_1:1;
hence contradiction by A6, A9; :: thesis:

end;

A46: C c= RightComp (Cage C,i) by A1, JORDAN10:11;
right_cell (Cage C,j),i1,(Gauge C,j) meets C by A1, A7, A8, JORDAN9:33;
then A47: C meets Cl (LeftComp (Cage C,i)) by A13, A14, XBOOLE_1:63;
A48: Cl (LeftComp (Cage C,i)) = (LeftComp (Cage C,i)) \/ (L~ (Cage C,i)) by GOBRD14:32;
C misses L~ (Cage C,i) by A1, JORDAN10:5;
then A49: C meets LeftComp (Cage C,i) by A47, A48, XBOOLE_1:70;
A50: LeftComp (Cage C,i) is_a_component_of D by GOBOARD9:def 1;
D = (LeftComp (Cage C,i)) \/ (RightComp (Cage C,i)) by GOBRD12:11;
then RightComp (Cage C,i) c= D by XBOOLE_1:7;
then A51: C c= D by A46, XBOOLE_1:1;
A52: RightComp (Cage C,i) is_a_component_of D by GOBOARD9:def 2;
C meets C ;
then C meets RightComp (Cage C,i) by A1, JORDAN10:11, XBOOLE_1:63;
hence contradiction by A1, A49, A50, A51, A52, JORDAN9:3, SPRECT_4:7; :: thesis: