let i be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL
for S being non empty Division of A
for D being Element of S st i in dom D holds
D . i in A
let A be closed-interval Subset of REAL ; :: thesis: for S being non empty Division of A
for D being Element of S st i in dom D holds
D . i in A
let S be non empty Division of A; :: thesis: for D being Element of S st i in dom D holds
D . i in A
let D be Element of S; :: 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 5;
rng D c= A by Def2;
hence D . i in A by A1; :: thesis: verum