let I be non empty closed_interval Subset of REAL; 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; ( divset (D,1) = [.(D . 1),(D . 1).] implies D . 1 = lower_bound I )
assume
divset (D,1) = [.(D . 1),(D . 1).]
; 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; verum