let j be Element of NAT ; :: thesis: for G being Matrix of (TOP-REAL 2) holds v_strip G,j is closed
let G be Matrix of (TOP-REAL 2); :: thesis: v_strip G,j is closed

now

per cases ( j < 1 or ( 1 <= j & j < len G ) or j >= len G ) ;

case A1: j < 1 ; :: thesis: v_strip G,j is closed

A2: now

assume j >= len G ; :: thesis: v_strip G,j is closed
then v_strip G,j = { |[s,r]| where s, r is Real : (G * j,1) `1 <= s } by GOBOARD5:def 1;
hence v_strip G,j is closed by Th15; :: thesis: verum

end;

now

assume j < len G ; :: thesis: v_strip G,j is closed
then v_strip G,j = { |[s,r]| where s, r is Real : s <= (G * (j + 1),1) `1 } by A1, GOBOARD5:def 1;
hence v_strip G,j is closed by Th14; :: thesis: verum

end;

hence v_strip G,j is closed by A2; :: thesis: verum

end;

case ( 1 <= j & j < len G ) ; :: thesis: v_strip G,j is closed

then A3: v_strip G,j = { |[s,r]| where s, r is Real : ( (G * j,1) `1 <= s & s <= (G * (j + 1),1) `1 ) } by GOBOARD5:def 1;
A4: { |[s,r]| where s, r is Real : ( (G * j,1) `1 <= s & s <= (G * (j + 1),1) `1 ) } = { |[s1,r1]| where s1, r1 is Real : (G * j,1) `1 <= s1 } /\ { |[s2,r2]| where s2, r2 is Real : s2 <= (G * (j + 1),1) `1 }

proof

A5: { |[s1,r1]| where s1, r1 is Real : (G * j,1) `1 <= s1 } /\ { |[s2,r2]| where s2, r2 is Real : s2 <= (G * (j + 1),1) `1 } c= { |[s,r]| where s, r is Real : ( (G * j,1) `1 <= s & s <= (G * (j + 1),1) `1 ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { |[s1,r1]| where s1, r1 is Real : (G * j,1) `1 <= s1 } /\ { |[s2,r2]| where s2, r2 is Real : s2 <= (G * (j + 1),1) `1 } or x in { |[s,r]| where s, r is Real : ( (G * j,1) `1 <= s & s <= (G * (j + 1),1) `1 ) } )
assume x in { |[s1,r1]| where s1, r1 is Real : (G * j,1) `1 <= s1 } /\ { |[s2,r2]| where s2, r2 is Real : s2 <= (G * (j + 1),1) `1 } ; :: thesis: x in { |[s,r]| where s, r is Real : ( (G * j,1) `1 <= s & s <= (G * (j + 1),1) `1 ) }
then A6: ( x in { |[s1,r1]| where s1, r1 is Real : (G * j,1) `1 <= s1 } & x in { |[s2,r2]| where s2, r2 is Real : s2 <= (G * (j + 1),1) `1 } ) by XBOOLE_0:def 4;
then ex s1, r1 being Real st
( |[s1,r1]| = x & (G * j,1) `1 <= s1 ) ;
then consider r1, s1 being Real such that
A7: ( |[s1,r1]| = x & (G * j,1) `1 <= s1 ) ;
consider s2, r2 being Real such that
A8: ( |[s2,r2]| = x & s2 <= (G * (j + 1),1) `1 ) by A6;
( r1 = r2 & s1 = s2 ) by A7, A8, SPPOL_2:1;
hence x in { |[s,r]| where s, r is Real : ( (G * j,1) `1 <= s & s <= (G * (j + 1),1) `1 ) } by A7, A8; :: thesis: verum

end;

A9: { |[s,r]| where s, r is Real : ( (G * j,1) `1 <= s & s <= (G * (j + 1),1) `1 ) } c= { |[s1,r1]| where s1, r1 is Real : s1 <= (G * (j + 1),1) `1 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { |[s,r]| where s, r is Real : ( (G * j,1) `1 <= s & s <= (G * (j + 1),1) `1 ) } or x in { |[s1,r1]| where s1, r1 is Real : s1 <= (G * (j + 1),1) `1 } )
assume x in { |[s,r]| where s, r is Real : ( (G * j,1) `1 <= s & s <= (G * (j + 1),1) `1 ) } ; :: thesis: x in { |[s1,r1]| where s1, r1 is Real : s1 <= (G * (j + 1),1) `1 }
then ex s, r being Real st
( x = |[s,r]| & (G * j,1) `1 <= s & s <= (G * (j + 1),1) `1 ) ;
hence x in { |[s1,r1]| where s1, r1 is Real : s1 <= (G * (j + 1),1) `1 } ; :: thesis: verum

end;

{ |[s,r]| where s, r is Real : ( (G * j,1) `1 <= s & s <= (G * (j + 1),1) `1 ) } c= { |[s1,r1]| where s1, r1 is Real : (G * j,1) `1 <= s1 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { |[s,r]| where s, r is Real : ( (G * j,1) `1 <= s & s <= (G * (j + 1),1) `1 ) } or x in { |[s1,r1]| where s1, r1 is Real : (G * j,1) `1 <= s1 } )
assume x in { |[s,r]| where s, r is Real : ( (G * j,1) `1 <= s & s <= (G * (j + 1),1) `1 ) } ; :: thesis: x in { |[s1,r1]| where s1, r1 is Real : (G * j,1) `1 <= s1 }
then ex s, r being Real st
( x = |[s,r]| & (G * j,1) `1 <= s & s <= (G * (j + 1),1) `1 ) ;
hence x in { |[s1,r1]| where s1, r1 is Real : (G * j,1) `1 <= s1 } ; :: thesis: verum

end;

then { |[s,r]| where s, r is Real : ( (G * j,1) `1 <= s & s <= (G * (j + 1),1) `1 ) } c= { |[s1,r1]| where s1, r1 is Real : (G * j,1) `1 <= s1 } /\ { |[s2,r2]| where s2, r2 is Real : s2 <= (G * (j + 1),1) `1 } by A9, XBOOLE_1:19;
hence { |[s,r]| where s, r is Real : ( (G * j,1) `1 <= s & s <= (G * (j + 1),1) `1 ) } = { |[s1,r1]| where s1, r1 is Real : (G * j,1) `1 <= s1 } /\ { |[s2,r2]| where s2, r2 is Real : s2 <= (G * (j + 1),1) `1 } by A5, XBOOLE_0:def 10; :: thesis: verum

end;

reconsider P1 = { |[s1,r1]| where s1, r1 is Real : (G * j,1) `1 <= s1 } as Subset of (TOP-REAL 2) by Lm9;
reconsider P2 = { |[s1,r1]| where s1, r1 is Real : s1 <= (G * (j + 1),1) `1 } as Subset of (TOP-REAL 2) by Lm7;
A10: P1 is closed by Th15;
P2 is closed by Th14;
hence v_strip G,j is closed by A3, A4, A10, TOPS_1:35; :: thesis: verum

end;

case j >= len G ; :: thesis: v_strip G,j is closed

then v_strip G,j = { |[s,r]| where s, r is Real : (G * j,1) `1 <= s } by GOBOARD5:def 1;
hence v_strip G,j is closed by Th15; :: thesis: verum

end;

end;

end;

hence v_strip G,j is closed ; :: thesis: verum