let i be Nat; :: thesis: for G being Matrix of (TOP-REAL 2) st 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: ( 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: ( 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, MATRIX_0:def 10;
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 object ; :: 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) by XBOOLE_0:def 4;
A8: x in v_strip (G,(i + 1)) by A6, 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 A9: i = 0 and
A10: 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, A9, Th10;
then consider r1, s1 being Real such that
A11: x = |[r1,s1]| and
A12: 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, Th9;
then consider r2, s2 being Real such that
A13: x = |[r2,s2]| and
A14: (G * ((i + 1),1)) `1 <= r2 by A8, A10;
r1 = |[r2,s2]| `1 by A11, A13, EUCLID:52
.= r2 by EUCLID:52 ;
then (G * ((i + 1),1)) `1 = r1 by A9, A12, A14, XXREAL_0:1;
then (G * ((i + 1),1)) `1 = p `1 by A11, EUCLID:52;
hence x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } ; :: thesis: verum

end;

suppose that A15: i = 0 and
A16: 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, A15, Th10;
then consider r1, s1 being Real such that
A17: x = |[r1,s1]| and
A18: r1 <= (G * (1,1)) `1 by A7;
i + 1 < len G by A3, A16, 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, A15, Th8;
then consider r2, s2 being Real such that
A19: x = |[r2,s2]| and
A20: (G * (1,1)) `1 <= r2 and
r2 <= (G * ((1 + 1),1)) `1 by A8;
r1 = |[r2,s2]| `1 by A17, A19, EUCLID:52
.= r2 by EUCLID:52 ;
then (G * (1,1)) `1 = r1 by A18, A20, XXREAL_0:1;
then (G * (1,1)) `1 = p `1 by A17, EUCLID:52;
hence x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } by A15; :: thesis: verum

end;

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

A23: 1 <= i by A21, NAT_1:14;
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, A23, Th8, A3, NAT_1:13;
then consider r1, s1 being Real such that
A24: x = |[r1,s1]| and
(G * (i,1)) `1 <= r1 and
A25: 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, Th9;
then consider r2, s2 being Real such that
A26: x = |[r2,s2]| and
A27: (G * ((i + 1),1)) `1 <= r2 by A8, A22;
r1 = |[r2,s2]| `1 by A24, A26, EUCLID:52
.= r2 by EUCLID:52 ;
then (G * ((i + 1),1)) `1 = r1 by A25, A27, XXREAL_0:1;
then (G * ((i + 1),1)) `1 = p `1 by A24, EUCLID:52;
hence x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } ; :: thesis: verum

end;

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

A30: 1 <= i by A28, NAT_1:14;
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, A30, Th8, A3, NAT_1:13;
then consider r1, s1 being Real such that
A31: x = |[r1,s1]| and
(G * (i,1)) `1 <= r1 and
A32: r1 <= (G * ((i + 1),1)) `1 by A7;
A33: 1 <= i + 1 by NAT_1:11;
i + 1 < len G by A3, A29, 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, A33, Th8;
then consider r2, s2 being Real such that
A34: x = |[r2,s2]| and
A35: (G * ((i + 1),1)) `1 <= r2 and
r2 <= (G * (((i + 1) + 1),1)) `1 by A8;
r1 = |[r2,s2]| `1 by A31, A34, EUCLID:52
.= r2 by EUCLID:52 ;
then (G * ((i + 1),1)) `1 = r1 by A32, A35, XXREAL_0:1;
then (G * ((i + 1),1)) `1 = p `1 by A31, EUCLID:52;
hence x in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 } ; :: thesis: verum

end;

end;

end;

A36: { 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 object ; :: 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
A37: p = x and
A38: p `1 = (G * ((i + 1),1)) `1 ;
A39: p = |[(p `1),(p `2)]| by EUCLID:53;

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

suppose A40: 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, Th10;
hence x in v_strip (G,i) by A37, A38, A39, A40; :: thesis: verum

end;

suppose A41: i >= 1 ; :: thesis: x in v_strip (G,i)

then A42: 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, Th8;
i < i + 1 by XREAL_1:29;
then (G * (i,1)) `1 < p `1 by A2, A3, A4, A38, A41, Th3;
hence x in v_strip (G,i) by A37, A38, A39, A42; :: 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 object ; :: 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
A43: p = x and
A44: p `1 = (G * ((i + 1),1)) `1 ;
A45: p = |[(p `1),(p `2)]| by EUCLID:53;
A46: 1 <= i + 1 by NAT_1:11;

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

suppose A47: 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, Th9;
hence x in v_strip (G,(i + 1)) by A43, A44, A45, A47; :: thesis: verum

end;

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

then A49: 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, A46, Th8;
A50: i + 1 < (i + 1) + 1 by NAT_1:13;
(i + 1) + 1 <= len G by A48, NAT_1:13;
then p `1 < (G * (((i + 1) + 1),1)) `1 by A2, A4, A44, A46, A50, Th3;
hence x in v_strip (G,(i + 1)) by A43, A44, A45, A49; :: 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 A36, XBOOLE_1:19; :: thesis: verum