k in NAT by ORDINAL1:def 12;
hence S . k is middle_volume of f,T . k by Def3; :: thesis: verum