for k being Element of NAT holds PFBrt (1,k) <> {{}}