let i be Element of NAT ; :: thesis: for G being Matrix of (TOP-REAL 2) st not G is empty-yielding & G is X_equal-in-line & G is X_increasing-in-column & i + 1 <= len G holds
(v_strip G,i) /\ (v_strip G,(i + 1)) = { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 }
let G be Matrix of (TOP-REAL 2); :: thesis: ( not G is empty-yielding & G is X_equal-in-line & G is X_increasing-in-column & i + 1 <= len G implies (v_strip G,i) /\ (v_strip G,(i + 1)) = { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 } )
assume that
A1: ( not G is empty-yielding & G is X_equal-in-line ) and
A2: G is X_increasing-in-column and
A3: i + 1 <= len G ; :: thesis: (v_strip G,i) /\ (v_strip G,(i + 1)) = { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 }
width G <> 0 by A1, GOBOARD1:def 5;
then A4: 1 <= width G by NAT_1:14;
A5: i < len G by A3, NAT_1:13;
thus (v_strip G,i) /\ (v_strip G,(i + 1)) c= { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 } :: according to XBOOLE_0:def 10 :: thesis: { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 } c= (v_strip G,i) /\ (v_strip G,(i + 1))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (v_strip G,i) /\ (v_strip G,(i + 1)) or x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 } )
assume A6: x in (v_strip G,i) /\ (v_strip G,(i + 1)) ; :: thesis: x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 }
then A7: ( x in v_strip G,i & x in v_strip G,(i + 1) ) by XBOOLE_0:def 4;
reconsider p = x as Point of (TOP-REAL 2) by A6;

per cases ( ( i = 0 & i + 1 = len G ) or ( i = 0 & i + 1 <> len G ) or ( i <> 0 & i + 1 = len G ) or ( i <> 0 & i + 1 <> len G ) ) ;

suppose that A8: i = 0 and
A9: i + 1 = len G ; :: thesis: x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 }

v_strip G,i = { |[r,s]| where r, s is Real : r <= (G * (0 + 1),1) `1 } by A1, A4, A8, Th11;
then consider r1, s1 being Real such that
A10: x = |[r1,s1]| and
A11: r1 <= (G * 1,1) `1 by A7;
v_strip G,(len G) = { |[r,s]| where r, s is Real : (G * (len G),1) `1 <= r } by A1, A4, Th10;
then consider r2, s2 being Real such that
A12: x = |[r2,s2]| and
A13: (G * (i + 1),1) `1 <= r2 by A7, A9;
r1 = |[r2,s2]| `1 by A10, A12, EUCLID:56
.= r2 by EUCLID:56 ;
then (G * (i + 1),1) `1 = r1 by A8, A11, A13, XXREAL_0:1;
then (G * (i + 1),1) `1 = p `1 by A10, EUCLID:56;
hence x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 } ; :: thesis: verum

end;

suppose that A14: i = 0 and
A15: i + 1 <> len G ; :: thesis: x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 }

v_strip G,i = { |[r,s]| where r, s is Real : r <= (G * (0 + 1),1) `1 } by A1, A4, A14, Th11;
then consider r1, s1 being Real such that
A16: x = |[r1,s1]| and
A17: r1 <= (G * 1,1) `1 by A7;
( 1 <= i + 1 & i + 1 < len G ) by A3, A15, NAT_1:11, XXREAL_0:1;
then v_strip G,(i + 1) = { |[r,s]| where r, s is Real : ( (G * (0 + 1),1) `1 <= r & r <= (G * ((0 + 1) + 1),1) `1 ) } by A1, A4, A14, Th9;
then consider r2, s2 being Real such that
A18: x = |[r2,s2]| and
A19: ( (G * 1,1) `1 <= r2 & r2 <= (G * (1 + 1),1) `1 ) by A7;
r1 = |[r2,s2]| `1 by A16, A18, EUCLID:56
.= r2 by EUCLID:56 ;
then (G * 1,1) `1 = r1 by A17, A19, XXREAL_0:1;
then (G * 1,1) `1 = p `1 by A16, EUCLID:56;
hence x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 } by A14; :: thesis: verum

end;

suppose that A20: i <> 0 and
A21: i + 1 = len G ; :: thesis: x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 }

( 1 <= i & i < len G ) by A3, A20, NAT_1:13, NAT_1:14;
then v_strip G,i = { |[r,s]| where r, s is Real : ( (G * i,1) `1 <= r & r <= (G * (i + 1),1) `1 ) } by A1, A4, Th9;
then consider r1, s1 being Real such that
A22: x = |[r1,s1]| and
A23: ( (G * i,1) `1 <= r1 & r1 <= (G * (i + 1),1) `1 ) by A7;
v_strip G,(len G) = { |[r,s]| where r, s is Real : (G * (len G),1) `1 <= r } by A1, A4, Th10;
then consider r2, s2 being Real such that
A24: x = |[r2,s2]| and
A25: (G * (i + 1),1) `1 <= r2 by A7, A21;
r1 = |[r2,s2]| `1 by A22, A24, EUCLID:56
.= r2 by EUCLID:56 ;
then (G * (i + 1),1) `1 = r1 by A23, A25, XXREAL_0:1;
then (G * (i + 1),1) `1 = p `1 by A22, EUCLID:56;
hence x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 } ; :: thesis: verum

end;

suppose that A26: i <> 0 and
A27: i + 1 <> len G ; :: thesis: x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 }

( 1 <= i & i < len G ) by A3, A26, NAT_1:13, NAT_1:14;
then v_strip G,i = { |[r,s]| where r, s is Real : ( (G * i,1) `1 <= r & r <= (G * (i + 1),1) `1 ) } by A1, A4, Th9;
then consider r1, s1 being Real such that
A28: x = |[r1,s1]| and
A29: ( (G * i,1) `1 <= r1 & r1 <= (G * (i + 1),1) `1 ) by A7;
( 1 <= i + 1 & i + 1 < len G ) by A3, A27, NAT_1:11, XXREAL_0:1;
then v_strip G,(i + 1) = { |[r,s]| where r, s is Real : ( (G * (i + 1),1) `1 <= r & r <= (G * ((i + 1) + 1),1) `1 ) } by A1, A4, Th9;
then consider r2, s2 being Real such that
A30: x = |[r2,s2]| and
A31: ( (G * (i + 1),1) `1 <= r2 & r2 <= (G * ((i + 1) + 1),1) `1 ) by A7;
r1 = |[r2,s2]| `1 by A28, A30, EUCLID:56
.= r2 by EUCLID:56 ;
then (G * (i + 1),1) `1 = r1 by A29, A31, XXREAL_0:1;
then (G * (i + 1),1) `1 = p `1 by A28, EUCLID:56;
hence x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 } ; :: thesis: verum

end;

end;

end;

A32: { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 } c= v_strip G,i

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 } or x in v_strip G,i )
assume x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 } ; :: thesis: x in v_strip G,i
then consider p being Point of (TOP-REAL 2) such that
A33: p = x and
A34: p `1 = (G * (i + 1),1) `1 ;
A35: p = |[(p `1 ),(p `2 )]| by EUCLID:57;

per cases ( i = 0 or i >= 1 ) by NAT_1:14;

suppose A36: i = 0 ; :: thesis: x in v_strip G,i

then v_strip G,i = { |[r,s]| where r, s is Real : r <= (G * 1,1) `1 } by A1, A4, Th11;
hence x in v_strip G,i by A33, A34, A35, A36; :: thesis: verum

end;

suppose A37: i >= 1 ; :: thesis: x in v_strip G,i

then A38: v_strip G,i = { |[r,s]| where r, s is Real : ( (G * i,1) `1 <= r & r <= (G * (i + 1),1) `1 ) } by A1, A4, A5, Th9;
i < i + 1 by XREAL_1:31;
then (G * i,1) `1 < p `1 by A2, A3, A4, A34, A37, Th4;
hence x in v_strip G,i by A33, A34, A35, A38; :: thesis: verum

end;

end;

end;

{ q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 } c= v_strip G,(i + 1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 } or x in v_strip G,(i + 1) )
assume x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 } ; :: thesis: x in v_strip G,(i + 1)
then consider p being Point of (TOP-REAL 2) such that
A39: p = x and
A40: p `1 = (G * (i + 1),1) `1 ;
A41: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
A42: 1 <= i + 1 by NAT_1:11;

per cases ( i + 1 = len G or i + 1 < len G ) by A3, XXREAL_0:1;

suppose A43: i + 1 = len G ; :: thesis: x in v_strip G,(i + 1)

then v_strip G,(i + 1) = { |[r,s]| where r, s is Real : (G * (len G),1) `1 <= r } by A1, A4, Th10;
hence x in v_strip G,(i + 1) by A39, A40, A41, A43; :: thesis: verum

end;

suppose A44: i + 1 < len G ; :: thesis: x in v_strip G,(i + 1)

then A45: v_strip G,(i + 1) = { |[r,s]| where r, s is Real : ( (G * (i + 1),1) `1 <= r & r <= (G * ((i + 1) + 1),1) `1 ) } by A1, A4, A42, Th9;
( i + 1 < (i + 1) + 1 & (i + 1) + 1 <= len G ) by A44, NAT_1:13;
then p `1 < (G * ((i + 1) + 1),1) `1 by A2, A4, A40, A42, Th4;
hence x in v_strip G,(i + 1) by A39, A40, A41, A45; :: thesis: verum

end;

end;

end;

hence { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 } c= (v_strip G,i) /\ (v_strip G,(i + 1)) by A32, XBOOLE_1:19; :: thesis: verum