let i be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL
for D being Division of A st i in dom D holds
divset D,i c= A
let A be closed-interval Subset of REAL ; :: thesis: for D being Division of A st i in dom D holds
divset D,i c= A
let D be Division of A; :: thesis: ( i in dom D implies divset D,i c= A )
assume A1: i in dom D ; :: thesis: divset D,i c= A

now

per cases ( i = 1 or i <> 1 ) ;

suppose A2: i = 1 ; :: thesis: divset D,i c= A

lower_bound A in A by RCOMP_1:32;
then A3: lower_bound A in [.(lower_bound A),(upper_bound A).] by Th5;
A4: lower_bound (divset D,i) = lower_bound A by A1, A2, Def5;
consider b being Real such that
A5: b = D . i ;
upper_bound (divset D,i) = b by A1, A2, A5, Def5;
then A6: divset D,i = [.(lower_bound A),b.] by A4, Th5;
b in A by A1, A5, Th8;
then b in [.(lower_bound A),(upper_bound A).] by Th5;
then [.(lower_bound A),b.] c= [.(lower_bound A),(upper_bound A).] by A3, XXREAL_2:def 12;
hence divset D,i c= A by A6, Th5; :: thesis: verum

end;

suppose A7: i <> 1 ; :: thesis: divset D,i c= A

consider b being Real such that
A8: b = D . i ;
b in A by A1, A8, Th8;
then A9: b in [.(lower_bound A),(upper_bound A).] by Th5;
consider a being Real such that
A10: a = D . (i - 1) ;
D . (i - 1) in A by A1, A7, Th9;
then a in [.(lower_bound A),(upper_bound A).] by A10, Th5;
then A11: [.a,b.] c= [.(lower_bound A),(upper_bound A).] by A9, XXREAL_2:def 12;
A12: upper_bound (divset D,i) = b by A1, A7, A8, Def5;
lower_bound (divset D,i) = a by A1, A7, A10, Def5;
then divset D,i = [.a,b.] by A12, Th5;
hence divset D,i c= A by A11, Th5; :: thesis: verum

end;

end;

end;

hence divset D,i c= A ; :: thesis: verum