let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A st 0 < vol A & D . 1 = lower_bound A holds
lower_bound A < (D /^ 1) . 1
let D be Division of A; :: thesis: ( 0 < vol A & D . 1 = lower_bound A implies lower_bound A < (D /^ 1) . 1 )
assume A1: ( 0 < vol A & D . 1 = lower_bound A ) ; :: thesis: lower_bound A < (D /^ 1) . 1
0 < len D ;
then A2: 0 + 1 <= len D by NAT_1:13;
1 <> len D

proof

assume 1 = len D ; :: thesis: contradiction
then D . 1 = upper_bound A by INTEGRA1:def 2;
hence contradiction by A1; :: thesis: verum

end;

then 1 < len D by A2, XXREAL_0:1;
then A4: 1 + 1 <= len D by NAT_1:13;
then A5: (1 + 1) - 1 <= (len D) - 1 by XREAL_1:9;
1 <= len (D /^ 1) by A5, A2, RFINSEQ:def 1;
then 1 in dom (D /^ 1) by FINSEQ_3:25;
then A9: (D /^ 1) . 1 = D . (1 + 1) by A2, RFINSEQ:def 1;
A10: 1 in dom D by FINSEQ_3:25, A2;
2 in dom D by A4, FINSEQ_3:25;
hence lower_bound A < (D /^ 1) . 1 by A1, A9, A10, VALUED_0:def 13; :: thesis: verum