hereby :: thesis: ( not i = 1 implies ex b₁ being non empty closed_interval Subset of REAL st
( lower_bound b₁ = D . (i - 1) & upper_bound b₁ = D . i ) )

assume i = 1 ; :: thesis: ex IT being non empty closed_interval Subset of REAL st
( lower_bound IT = lower_bound A & upper_bound IT = D . i )
thus ex IT being non empty closed_interval Subset of REAL st
( lower_bound IT = lower_bound A & upper_bound IT = D . i ) :: thesis: verum

proof

consider I being Subset of REAL such that
A2: I = [.(lower_bound A),(D . i).] ;
D . i in A by A1, Th4;
then lower_bound A <= D . i by SEQ_4:def 2;
then A3: I is non empty closed_interval Subset of REAL by A2, MEASURE5:14;
then A4: I = [.(lower_bound I),(upper_bound I).] by Th2;
then A5: upper_bound I = D . i by A2, A3, Th3;
lower_bound I = lower_bound A by A2, A3, A4, Th3;
hence ex IT being non empty closed_interval Subset of REAL st
( lower_bound IT = lower_bound A & upper_bound IT = D . i ) by A3, A5; :: thesis: verum

end;

end;

assume A6: i <> 1 ; :: thesis: ex b₁ being non empty closed_interval Subset of REAL st
( lower_bound b₁ = D . (i - 1) & upper_bound b₁ = D . i )
thus ex IT being non empty closed_interval Subset of REAL st
( lower_bound IT = D . (i - 1) & upper_bound IT = D . i ) :: thesis: verum

proof

reconsider j = i - 1 as Element of NAT by A1, A6, Th5;
A7: i + (- 1) < i + (1 + (- 1)) by XREAL_1:6;
consider a1, b1 being Real such that
A8: a1 = D . (i - 1) and
A9: b1 = D . i ;
consider I being Subset of REAL such that
A10: I = [.a1,b1.] ;
i - 1 in dom D by A1, A6, Th5;
then D . j < D . i by A1, A7, SEQM_3:def 1;
then A11: I is non empty closed_interval Subset of REAL by A8, A9, A10, MEASURE5:14;
then A12: I = [.(lower_bound I),(upper_bound I).] by Th2;
then A13: upper_bound I = D . i by A9, A10, A11, Th3;
lower_bound I = D . (i - 1) by A8, A10, A11, A12, Th3;
hence ex IT being non empty closed_interval Subset of REAL st
( lower_bound IT = D . (i - 1) & upper_bound IT = D . i ) by A11, A13; :: thesis: verum

end;