theorem Th17: :: NUMBER13:17

for m, n being Nat st m <= n holds
(primesFinS n) | m = primesFinS m