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