theorem :: HEYTING3:26

for k being Element of NAT holds PFBrt (1,k) = {(PFArt (1,k)),(PFCrt (1,k))}