:: deftheorem Def5 defines PFDrt HEYTING3:def 5 :
for k being Element of NAT
for b₂ being Subset of (SubstPoset (NAT,{k})) holds
( b₂ = PFDrt k iff for x being object holds
( x in b₂ iff ex n being non zero Element of NAT st x = PFBrt (n,k) ) );