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

set b = D . i;
D . i in A by A1, Th8;
then A9: D . i in [.(lower_bound A),(upper_bound A).] by Th5;
set a = D . (i - 1);
D . (i - 1) in A by A1, A7, Th9;
then D . (i - 1) in [.(lower_bound A),(upper_bound A).] by Th5;
then A11: [.(D . (i - 1)),(D . i).] c= [.(lower_bound A),(upper_bound A).] by A9, XXREAL_2:def 12;
A12: upper_bound (divset (D,i)) = D . i by A1, A7, Def5;
lower_bound (divset (D,i)) = D . (i - 1) by A1, A7, Def5;
then divset (D,i) = [.(D . (i - 1)),(D . i).] 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