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

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 ) )end;

hence
v_strip (G,j) is closed
; :: thesis: verumper cases
( j < 1 or ( 1 <= j & j < len G ) or j >= len G )
;

end;

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

end;

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;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

now :: thesis: ( j < len G implies v_strip (G,j) is closed )

hence
v_strip (G,j) is closed
by A2; :: thesis: verumassume
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;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

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 }

hence v_strip (G,j) is closed by A3, A4, TOPS_1:8; :: thesis: verum

end;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

( P1 is closed & P2 is closed )
by Th14, Th15;
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 ) }

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;proof

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 }
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;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

proof

{ |[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 }
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;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

proof

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;
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;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

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

hence v_strip (G,j) is closed by A3, A4, TOPS_1:8; :: thesis: verum