theorem Th25: :: HEYTING3:25

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