let a, b be Real; :: thesis: for Iab being non empty closed_interval Subset of REAL st a <= b & Iab = [.a,b.] holds
for Dab being Division of Iab st len Dab = 1 holds
Dab = <*b*>
let Iab be non empty closed_interval Subset of REAL; :: thesis: ( a <= b & Iab = [.a,b.] implies for Dab being Division of Iab st len Dab = 1 holds
Dab = <*b*> )
assume that
A1: a <= b and
A2: Iab = [.a,b.] ; :: thesis: for Dab being Division of Iab st len Dab = 1 holds
Dab = <*b*>
let Dab be Division of Iab; :: thesis: ( len Dab = 1 implies Dab = <*b*> )
assume A3: len Dab = 1 ; :: thesis: Dab = <*b*>
then consider d being Real such that
A4: Dab = <*(Dab . 1)*> by FINSEQ_1:40;
Dab . 1 = upper_bound Iab by A3, INTEGRA1:def 2
.= b by A1, A2, JORDAN5A:19 ;
hence Dab = <*b*> by A4; :: thesis: verum