:: deftheorem defDp2 defines Dp2 DUALSP05:def 3 :
for A being non empty closed_interval Subset of REAL
for D being Division of A
for rho being Function of A,REAL
for i being Nat holds
( ( i = 1 implies Dp2 (rho,D,i) = rho . (lower_bound A) ) & ( not i = 1 implies Dp2 (rho,D,i) = rho . (D . (i - 1)) ) );