let i, j be Element of NAT ; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds
L~ (Cage C,j) c= Cl (RightComp (Cage C,i))
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( C is connected & i <= j implies L~ (Cage C,j) c= Cl (RightComp (Cage C,i)) )
assume that
A1: C is connected and
A2: i <= j and
A3: not L~ (Cage C,j) c= Cl (RightComp (Cage C,i)) ; :: thesis: contradiction
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 GOBOARD1:2;
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 ( ( i4 = i5 & j4 + 1 = j5 ) or ( i4 + 1 = i5 & j4 = j5 ) or ( i4 = i5 + 1 & j4 = j5 ) or ( i4 = i5 & j4 = j5 + 1 ) ) by A26, GOBOARD1:1;

suppose A30: ( i4 = i5 & j4 + 1 = j5 ) ; :: 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 )

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: verum

end;

suppose A31: ( i4 + 1 = i5 & j4 = j5 ) ; :: 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 )

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: verum

end;

suppose A33: ( i4 = i5 + 1 & j4 = j5 ) ; :: 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 )

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: verum

end;

suppose A34: ( i4 = i5 & j4 = j5 + 1 ) ; :: 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 )

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: verum

end;

end;

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: contradiction
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: verum

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: verum