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

assume ( 1 <= i & i < len G ) ; :: thesis: { |[r,s]| where r, s is Real : ( (G * i,1) `1 <= r & r <= (G * (i + 1),1) `1 ) } is Subset of (TOP-REAL 2)
set A = { |[r,s]| where r, s is Real : ( (G * i,1) `1 <= r & r <= (G * (i + 1),1) `1 ) } ;
{ |[r,s]| where r, s is Real : ( (G * i,1) `1 <= r & r <= (G * (i + 1),1) `1 ) } 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 * i,1) `1 <= r & r <= (G * (i + 1),1) `1 ) } or x in the carrier of (TOP-REAL 2) )
assume x in { |[r,s]| where r, s is Real : ( (G * i,1) `1 <= r & r <= (G * (i + 1),1) `1 ) } ; :: thesis: x in the carrier of (TOP-REAL 2)
then ex r, s being Real st
( x = |[r,s]| & (G * i,1) `1 <= r & r <= (G * (i + 1),1) `1 ) ;
hence x in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;

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

end;

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

assume i >= len G ; :: thesis: { |[r,s]| where r, s is Real : (G * i,1) `1 <= r } is Subset of (TOP-REAL 2)
set A = { |[r,s]| where r, s is Real : (G * i,1) `1 <= r } ;
{ |[r,s]| where r, s is Real : (G * i,1) `1 <= r } 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 * i,1) `1 <= r } or x in the carrier of (TOP-REAL 2) )
assume x in { |[r,s]| where r, s is Real : (G * i,1) `1 <= r } ; :: thesis: x in the carrier of (TOP-REAL 2)
then ex r, s being Real st
( x = |[r,s]| & (G * i,1) `1 <= r ) ;
hence x in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;

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

end;

assume ( ( not 1 <= i or not i < len G ) & i < len G ) ; :: thesis: { |[r,s]| where r, s is Real : r <= (G * (i + 1),1) `1 } is Subset of (TOP-REAL 2)
set A = { |[r,s]| where r, s is Real : r <= (G * (i + 1),1) `1 } ;
{ |[r,s]| where r, s is Real : r <= (G * (i + 1),1) `1 } 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 : r <= (G * (i + 1),1) `1 } or x in the carrier of (TOP-REAL 2) )
assume x in { |[r,s]| where r, s is Real : r <= (G * (i + 1),1) `1 } ; :: thesis: x in the carrier of (TOP-REAL 2)
then ex r, s being Real st
( x = |[r,s]| & r <= (G * (i + 1),1) `1 ) ;
hence x in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;

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