let j be Element of NAT ; :: thesis: for G being Matrix of (TOP-REAL 2) st not 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: ( not 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: ( not 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, GOBOARD1:def 5;
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 set ; :: 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 & x in h_strip G,(j + 1) ) by 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 A8: j = 0 and
A9: 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, A8, Th8;
then consider r1, s1 being Real such that
A10: x = |[r1,s1]| and
A11: 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, Th7;
then consider r2, s2 being Real such that
A12: x = |[r2,s2]| and
A13: (G * 1,(j + 1)) `2 <= s2 by A7, A9;
s1 = |[r2,s2]| `2 by A10, A12, EUCLID:56
.= s2 by EUCLID:56 ;
then (G * 1,(j + 1)) `2 = s1 by A8, A11, A13, XXREAL_0:1;
then (G * 1,(j + 1)) `2 = p `2 by A10, EUCLID:56;
hence x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * 1,(j + 1)) `2 } ; :: thesis: verum

end;

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

end;

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

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

end;

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

( 1 <= j & j < width G ) by A3, A26, NAT_1:13, NAT_1:14;
then 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, Th6;
then consider r1, s1 being Real such that
A28: x = |[r1,s1]| and
A29: ( (G * 1,j) `2 <= s1 & s1 <= (G * 1,(j + 1)) `2 ) by A7;
( 1 <= j + 1 & j + 1 < width G ) by A3, A27, NAT_1:11, 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, Th6;
then consider r2, s2 being Real such that
A30: x = |[r2,s2]| and
A31: ( (G * 1,(j + 1)) `2 <= s2 & s2 <= (G * 1,((j + 1) + 1)) `2 ) by A7;
s1 = |[r2,s2]| `2 by A28, A30, EUCLID:56
.= s2 by EUCLID:56 ;
then (G * 1,(j + 1)) `2 = s1 by A29, A31, XXREAL_0:1;
then (G * 1,(j + 1)) `2 = p `2 by A28, EUCLID:56;
hence x in { q where q is Point of (TOP-REAL 2) : q `2 = (G * 1,(j + 1)) `2 } ; :: thesis: verum

end;

end;

end;

A32: { 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 set ; :: 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
A33: p = x and
A34: p `2 = (G * 1,(j + 1)) `2 ;
A35: p = |[(p `1 ),(p `2 )]| by EUCLID:57;

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

suppose A36: 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, Th8;
hence x in h_strip G,j by A33, A34, A35, A36; :: thesis: verum

end;

suppose A37: j >= 1 ; :: thesis: x in h_strip G,j

then A38: 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, Th6;
j < j + 1 by XREAL_1:31;
then (G * 1,j) `2 < p `2 by A2, A3, A4, A34, A37, Th5;
hence x in h_strip G,j by A33, A34, A35, A38; :: 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 set ; :: 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
A39: p = x and
A40: p `2 = (G * 1,(j + 1)) `2 ;
A41: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
A42: 1 <= j + 1 by NAT_1:11;

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

suppose A43: 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, Th7;
hence x in h_strip G,(j + 1) by A39, A40, A41, A43; :: thesis: verum

end;

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

then A45: 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, A42, Th6;
( j + 1 < (j + 1) + 1 & (j + 1) + 1 <= width G ) by A44, NAT_1:13;
then p `2 < (G * 1,((j + 1) + 1)) `2 by A2, A4, A40, A42, Th5;
hence x in h_strip G,(j + 1) by A39, A40, A41, A45; :: 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 A32, XBOOLE_1:19; :: thesis: verum