:: deftheorem defines |-count NEWTON03:def 6 :
for a, b being Integer holds a |-count b = |.a.| |-count |.b.|;