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

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

proof

A2: D . i in A by A1, Th8;
consider I being Subset of REAL such that
A3: I = [.(lower_bound A),(D . i).] ;
lower_bound A <= D . i by A2, SEQ_4:def 5;
then A4: I is closed-interval Subset of REAL by A3, Def1;
( lower_bound I = lower_bound A & upper_bound I = D . i )

proof

I = [.(lower_bound I),(upper_bound I).] by A4, Th5;
hence ( lower_bound I = lower_bound A & upper_bound I = D . i ) by A3, A4, Th6; :: thesis: verum

end;

hence ex IT being closed-interval Subset of REAL st
( lower_bound IT = lower_bound A & upper_bound IT = D . i ) by A4; :: thesis: verum

end;

end;

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

proof

A6: ( i - 1 in dom D & D . (i - 1) in A ) by A1, A5, Th9;
A7: i + (- 1) < i + (1 + (- 1)) by XREAL_1:8;
consider a1, b1 being Real such that
A8: ( a1 = D . (i - 1) & b1 = D . i ) ;
reconsider j = i - 1 as Element of NAT by A1, A5, Th9;
A9: D . j < D . i by A1, A6, A7, SEQM_3:def 1;
consider I being Subset of REAL such that
A10: I = [.a1,b1.] ;
A11: I is closed-interval Subset of REAL by A8, A9, A10, Def1;
then I = [.(lower_bound I),(upper_bound I).] by Th5;
then ( lower_bound I = D . (i - 1) & upper_bound I = D . i ) by A8, A10, A11, Th6;
hence ex IT being closed-interval Subset of REAL st
( lower_bound IT = D . (i - 1) & upper_bound IT = D . i ) by A11; :: thesis: verum

end;