theorem :: HEYTING3:20

for n being Element of NAT holds PFArt (1,n) = {[1,n],[2,n]}