for n, k being Element of NAT holds PFBrt (n,k) is Element of (SubstPoset (NAT,{k}))