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