let a, b be Real; for Iab being non empty closed_interval Subset of REAL st a < b & Iab = [.a,b.] holds
<*a,b*> is Division of Iab
let Iab be non empty closed_interval Subset of REAL; ( a < b & Iab = [.a,b.] implies <*a,b*> is Division of Iab )
assume that
A1:
a < b
and
A2:
Iab = [.a,b.]
; <*a,b*> is Division of Iab
set D = <*a,b*>;
A3:
<*a,b*> is non empty increasing FinSequence of REAL
by A1, Th45;
A4:
rng <*a,b*> c= Iab
<*a,b*> . (len <*a,b*>) = upper_bound Iab
hence
<*a,b*> is Division of Iab
by A3, A4, INTEGRA1:def 2; verum