let i be Element of NAT ; :: thesis: for A being non empty 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 non empty 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 :: thesis: divset (D,i) c= A

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:14;
then A3: lower_bound A in [.(lower_bound A),(upper_bound A).] by Th2;
A4: lower_bound (divset (D,i)) = lower_bound A by A1, A2, Def3;
consider b being Real such that
A5: b = D . i ;
upper_bound (divset (D,i)) = b by A1, A2, A5, Def3;
then A6: divset (D,i) = [.(lower_bound A),b.] by A4, Th2;
b in A by A1, A5, Th4;
then b in [.(lower_bound A),(upper_bound A).] by Th2;
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, Th2; :: thesis: verum

end;

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

set b = D . i;
D . i in A by A1, Th4;
then A8: D . i in [.(lower_bound A),(upper_bound A).] by Th2;
set a = D . (i - 1);
D . (i - 1) in A by A1, A7, Th5;
then D . (i - 1) in [.(lower_bound A),(upper_bound A).] by Th2;
then A9: [.(D . (i - 1)),(D . i).] c= [.(lower_bound A),(upper_bound A).] by A8, XXREAL_2:def 12;
A10: upper_bound (divset (D,i)) = D . i by A1, A7, Def3;
lower_bound (divset (D,i)) = D . (i - 1) by A1, A7, Def3;
then divset (D,i) = [.(D . (i - 1)),(D . i).] by A10, Th2;
hence divset (D,i) c= A by A9, Th2; :: thesis: verum

end;

end;

end;

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