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

proof

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

per cases ( ( j = 0 & j + 1 = width G ) or ( j = 0 & j + 1 <> width G ) or ( j <> 0 & j + 1 = width G ) or ( j <> 0 & j + 1 <> width G ) ) ;

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

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

end;

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

h_strip (G,j) = { |[r,s]| where r, s is Real : s <= (G * (1,(0 + 1))) `2 } by A1, A4, A15, Th7;
then consider r1, s1 being Real such that
A17: x = |[r1,s1]| and
A18: s1 <= (G * (1,1)) `2 by A7;
j + 1 < width G by A3, A16, XXREAL_0:1;
then h_strip (G,(j + 1)) = { |[r,s]| where r, s is Real : ( (G * (1,(0 + 1))) `2 <= s & s <= (G * (1,((0 + 1) + 1))) `2 ) } by A1, A4, A15, Th5;
then consider r2, s2 being Real such that
A19: x = |[r2,s2]| and
A20: (G * (1,1)) `2 <= s2 and
s2 <= (G * (1,(1 + 1))) `2 by A8;
s1 = |[r2,s2]| `2 by A17, A19, EUCLID:52
.= s2 by EUCLID:52 ;
then (G * (1,1)) `2 = s1 by A18, A20, XXREAL_0:1;
then (G * (1,1)) `2 = p `2 by A17, EUCLID:52;
hence x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } by A15; :: thesis: verum

end;

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

A23: 1 <= j by A21, NAT_1:14;
h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by A1, A4, A23, Th5, A3, NAT_1:13;
then consider r1, s1 being Real such that
A24: x = |[r1,s1]| and
(G * (1,j)) `2 <= s1 and
A25: s1 <= (G * (1,(j + 1))) `2 by A7;
h_strip (G,(width G)) = { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s } by A1, A4, Th6;
then consider r2, s2 being Real such that
A26: x = |[r2,s2]| and
A27: (G * (1,(j + 1))) `2 <= s2 by A8, A22;
s1 = |[r2,s2]| `2 by A24, A26, EUCLID:52
.= s2 by EUCLID:52 ;
then (G * (1,(j + 1))) `2 = s1 by A25, A27, XXREAL_0:1;
then (G * (1,(j + 1))) `2 = p `2 by A24, EUCLID:52;
hence x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } ; :: thesis: verum

end;

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

A30: 1 <= j by A28, NAT_1:14;
h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by A1, A4, A30, Th5, A3, NAT_1:13;
then consider r1, s1 being Real such that
A31: x = |[r1,s1]| and
(G * (1,j)) `2 <= s1 and
A32: s1 <= (G * (1,(j + 1))) `2 by A7;
A33: 1 <= j + 1 by NAT_1:11;
j + 1 < width G by A3, A29, XXREAL_0:1;
then h_strip (G,(j + 1)) = { |[r,s]| where r, s is Real : ( (G * (1,(j + 1))) `2 <= s & s <= (G * (1,((j + 1) + 1))) `2 ) } by A1, A4, A33, Th5;
then consider r2, s2 being Real such that
A34: x = |[r2,s2]| and
A35: (G * (1,(j + 1))) `2 <= s2 and
s2 <= (G * (1,((j + 1) + 1))) `2 by A8;
s1 = |[r2,s2]| `2 by A31, A34, EUCLID:52
.= s2 by EUCLID:52 ;
then (G * (1,(j + 1))) `2 = s1 by A32, A35, XXREAL_0:1;
then (G * (1,(j + 1))) `2 = p `2 by A31, EUCLID:52;
hence x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } ; :: thesis: verum

end;

end;

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } or x in h_strip (G,j) )
assume x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } ; :: thesis: x in h_strip (G,j)
then consider p being Point of (TOP-REAL 2) such that
A37: p = x and
A38: p `2 = (G * (1,(j + 1))) `2 ;
A39: p = |[(p `1),(p `2)]| by EUCLID:53;

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

suppose A40: j = 0 ; :: thesis: x in h_strip (G,j)

then h_strip (G,j) = { |[r,s]| where r, s is Real : s <= (G * (1,1)) `2 } by A1, A4, Th7;
hence x in h_strip (G,j) by A37, A38, A39, A40; :: thesis: verum

end;

suppose A41: j >= 1 ; :: thesis: x in h_strip (G,j)

then A42: h_strip (G,j) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) } by A1, A4, A5, Th5;
j < j + 1 by XREAL_1:29;
then (G * (1,j)) `2 < p `2 by A2, A3, A4, A38, A41, Th4;
hence x in h_strip (G,j) by A37, A38, A39, A42; :: thesis: verum

end;

end;

end;

{ q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } c= h_strip (G,(j + 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 `2 = (G * (1,(j + 1))) `2 } or x in h_strip (G,(j + 1)) )
assume x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 } ; :: thesis: x in h_strip (G,(j + 1))
then consider p being Point of (TOP-REAL 2) such that
A43: p = x and
A44: p `2 = (G * (1,(j + 1))) `2 ;
A45: p = |[(p `1),(p `2)]| by EUCLID:53;
A46: 1 <= j + 1 by NAT_1:11;

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

suppose A47: j + 1 = width G ; :: thesis: x in h_strip (G,(j + 1))

then h_strip (G,(j + 1)) = { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 <= s } by A1, A4, Th6;
hence x in h_strip (G,(j + 1)) by A43, A44, A45, A47; :: thesis: verum

end;

suppose A48: j + 1 < width G ; :: thesis: x in h_strip (G,(j + 1))

then A49: h_strip (G,(j + 1)) = { |[r,s]| where r, s is Real : ( (G * (1,(j + 1))) `2 <= s & s <= (G * (1,((j + 1) + 1))) `2 ) } by A1, A4, A46, Th5;
A50: j + 1 < (j + 1) + 1 by NAT_1:13;
(j + 1) + 1 <= width G by A48, NAT_1:13;
then p `2 < (G * (1,((j + 1) + 1))) `2 by A2, A4, A44, A46, A50, Th4;
hence x in h_strip (G,(j + 1)) by A43, A44, A45, A49; :: thesis: verum

end;

end;

end;

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