theorem Th28: :: HEYTING3:28

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