let n, m be Nat; :: thesis: ( n <= m implies Product (primesFinS n) <= Product (primesFinS m) )
assume n <= m ; :: thesis: Product (primesFinS n) <= Product (primesFinS m)
then (primesFinS m) | n = primesFinS n by NUMBER13:17;
hence Product (primesFinS n) <= Product (primesFinS m) by NUMBER13:22; :: thesis: verum