defpred S₁[ Element of NAT , Subset of REAL] means $2 = (G . ((pr1 H) . $1)) . ((pr2 H) . $1);
A2: for n being Element of NAT ex y being Subset of REAL st S₁[n,y] ;
consider GG being sequence of (bool REAL) such that
A3: for n being Element of NAT holds S₁[n,GG . n] from FUNCT_2:sch 3(A2);
A4: union (rng F) c= union (rng GG)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng F) or x in union (rng GG) )
assume x in union (rng F) ; :: thesis: x in union (rng GG)
then consider A being set such that
A5: x in A and
A6: A in rng F by TARSKI:def 4;
consider n1 being object such that
A7: n1 in dom F and
A8: A = F . n1 by A6, FUNCT_1:def 3;
reconsider n1 = n1 as Element of NAT by A7;
F . n1 c= union (rng (G . n1)) by Def2;
then consider AA being set such that
A9: x in AA and
A10: AA in rng (G . n1) by A5, A8, TARSKI:def 4;
consider n2 being object such that
A11: n2 in dom (G . n1) and
A12: AA = (G . n1) . n2 by A10, FUNCT_1:def 3;
reconsider n2 = n2 as Element of NAT by A11;
consider n being object such that
A13: n in dom H and
A14: [n1,n2] = H . n by A1, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A13;
[((pr1 H) . n),((pr2 H) . n)] = [n1,n2] by A14, FUNCT_2:119;
then ( (pr1 H) . n = n1 & (pr2 H) . n = n2 ) by XTUPLE_0:1;
then A15: x in GG . n by A3, A9, A12;
GG . n in rng GG by FUNCT_2:4;
hence x in union (rng GG) by A15, TARSKI:def 4; :: thesis: verum

end;

for n being Element of NAT holds GG . n is Interval

proof

let n be Element of NAT ; :: thesis: GG . n is Interval
GG . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) by A3;
hence GG . n is Interval ; :: thesis: verum

end;

then reconsider GG = GG as Interval_Covering of union (rng F) by A4, Def2;
take GG ; :: thesis: for n being Element of NAT holds GG . n = (G . ((pr1 H) . n)) . ((pr2 H) . n)
thus for n being Element of NAT holds GG . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) by A3; :: thesis: verum