hereby :: thesis: ( ( i >= width G implies { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } is Subset of (TOP-REAL 2) ) & ( ( not 1 <= i or not i < width G ) & not i >= width G implies { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } is Subset of (TOP-REAL 2) ) )

assume that
1 <= i and
i < width G ; :: thesis: { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } is Subset of (TOP-REAL 2)
set A = { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } ;
{ |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } c= the carrier of (TOP-REAL 2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } or x in the carrier of (TOP-REAL 2) )
assume x in { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } ; :: thesis: x in the carrier of (TOP-REAL 2)
then ex r, s being Real st
( x = |[r,s]| & (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) ;
hence x in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;

hence { |[r,s]| where r, s is Real : ( (G * (1,i)) `2 <= s & s <= (G * (1,(i + 1))) `2 ) } is Subset of (TOP-REAL 2) ; :: thesis: verum

end;

hereby :: thesis: ( ( not 1 <= i or not i < width G ) & not i >= width G implies { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } is Subset of (TOP-REAL 2) )

assume i >= width G ; :: thesis: { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } is Subset of (TOP-REAL 2)
set A = { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } ;
{ |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } c= the carrier of (TOP-REAL 2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } or x in the carrier of (TOP-REAL 2) )
assume x in { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } ; :: thesis: x in the carrier of (TOP-REAL 2)
then ex r, s being Real st
( x = |[r,s]| & (G * (1,i)) `2 <= s ) ;
hence x in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;

hence { |[r,s]| where r, s is Real : (G * (1,i)) `2 <= s } is Subset of (TOP-REAL 2) ; :: thesis: verum

end;

assume that
( not 1 <= i or not i < width G ) and
i < width G ; :: thesis: { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } is Subset of (TOP-REAL 2)
set A = { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } ;
{ |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } c= the carrier of (TOP-REAL 2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } or x in the carrier of (TOP-REAL 2) )
assume x in { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } ; :: thesis: x in the carrier of (TOP-REAL 2)
then ex r, s being Real st
( x = |[r,s]| & s <= (G * (1,(i + 1))) `2 ) ;
hence x in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;

hence { |[r,s]| where r, s is Real : s <= (G * (1,(i + 1))) `2 } is Subset of (TOP-REAL 2) ; :: thesis: verum