for n, m, k being Element of NAT st n <= k holds
PFCrt (n,m) c= PFCrt (k,m)