theorem Count7: :: NEWTON03:92

for a, b being non trivial Nat
for c being non zero Nat holds a |^ ((a |-count b) * (b |-count c)) <= c