let I be non empty closed_interval Subset of REAL; :: thesis: for D being Division of I st divset (D,1) = [.(D . 1),(D . 1).] holds
D . 1 = lower_bound I
let D be Division of I; :: thesis: ( divset (D,1) = [.(D . 1),(D . 1).] implies D . 1 = lower_bound I )
assume divset (D,1) = [.(D . 1),(D . 1).] ; :: thesis: D . 1 = lower_bound I
then A1: ( lower_bound (divset (D,1)) = D . 1 & upper_bound (divset (D,1)) = D . 1 ) by JORDAN5A:19;
A2: divset (D,1) = [.(lower_bound I),(D . 1).] by COUSIN:50;
rng D <> {} ;
then 1 in dom D by FINSEQ_3:32;
then D . 1 in I by INTEGRA1:6;
then D . 1 in [.(lower_bound I),(upper_bound I).] by INTEGRA1:4;
then ( lower_bound I <= D . 1 & D . 1 <= upper_bound I ) by XXREAL_1:1;
hence D . 1 = lower_bound I by A1, A2, JORDAN5A:19; :: thesis: verum