let j be 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 :: thesis: ( ( j < 1 & v_strip (G,j) is closed ) or ( 1 <= j & j < len G & v_strip (G,j) is closed ) or ( j >= len G & v_strip (G,j) is closed ) )
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 :: thesis: ( j >= len G implies v_strip (G,j) is closed )
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 :: thesis: ( j < len G implies v_strip (G,j) is closed )
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;
reconsider P2 = { |[s1,r1]| where s1, r1 is Real : s1 <= (G * ((j + 1),1)) `1 } as Subset of (TOP-REAL 2) by Lm7;
reconsider P1 = { |[s1,r1]| where s1, r1 is Real : (G * (j,1)) `1 <= s1 } as Subset of (TOP-REAL 2) by Lm9;
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 object ; :: 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 A6: 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 A7: x in { |[s2,r2]| where s2, r2 is Real : s2 <= (G * ((j + 1),1)) `1 } by XBOOLE_0:def 4;
x in { |[s1,r1]| where s1, r1 is Real : (G * (j,1)) `1 <= s1 } by A6, 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
A8: |[s1,r1]| = x and
A9: (G * (j,1)) `1 <= s1 ;
consider s2, r2 being Real such that
A10: |[s2,r2]| = x and
A11: s2 <= (G * ((j + 1),1)) `1 by A7;
s1 = s2 by A8, A10, 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 A8, A9, A11; :: thesis: verum
end;
A12: { |[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 object ; :: 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;
{ |[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 object ; :: 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;
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 A12, 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; :: thesis: verum
end;
( P1 is closed & P2 is closed ) by Th14, Th15;
hence v_strip (G,j) is closed by A3, A4, TOPS_1:8; :: 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