let i be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL
for S being non empty Division of A
for D being Element of S st i in dom D holds
divset D,i c= A
let A be closed-interval Subset of REAL ; :: thesis: for S being non empty Division of A
for D being Element of S st i in dom D holds
divset D,i c= A
let S be non empty Division of A; :: thesis: for D being Element of S st i in dom D holds
divset D,i c= A
let D be Element of S; :: 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

consider b being Real such that
A3: b = D . i ;
A4: lower_bound (divset D,i) = lower_bound A by A1, A2, Def5;
upper_bound (divset D,i) = b by A1, A2, A3, Def5;
then A5: divset D,i = [.(lower_bound A),b.] by A4, Th5;
A6: lower_bound A in [.(lower_bound A),(upper_bound A).]

proof

lower_bound A in A by RCOMP_1:32;
hence lower_bound A in [.(lower_bound A),(upper_bound A).] by Th5; :: thesis: verum

end;

b in [.(lower_bound A),(upper_bound A).]

proof

b in A by A1, A3, Th8;
hence b in [.(lower_bound A),(upper_bound A).] by Th5; :: thesis: verum

end;

then [.(lower_bound A),b.] c= [.(lower_bound A),(upper_bound A).] by A6, XXREAL_2:def 12;
hence divset D,i c= A by A5, Th5; :: thesis: verum

end;

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

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

proof

b in A by A1, A11, Th8;
hence b in [.(lower_bound A),(upper_bound A).] by Th5; :: thesis: verum

end;

then [.a,b.] c= [.(lower_bound A),(upper_bound A).] by A13, XXREAL_2:def 12;
hence divset D,i c= A by A12, Th5; :: thesis: verum

end;

end;

end;

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