let i be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL
for D being Division of A st i in dom D holds
D . i in A
let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A st i in dom D holds
D . i in A
let D be Division of A; :: thesis: ( i in dom D implies D . i in A )
assume i in dom D ; :: thesis: D . i in A
then A1: D . i in rng D by FUNCT_1:def 3;
rng D c= A by Def1;
hence D . i in A by A1; :: thesis: verum