:: deftheorem Def3 defines PFCrt HEYTING3:def 3 :
for n, k being Nat
for b₃ being Element of PFuncs (NAT,{k}) holds
( b₃ = PFCrt (n,k) iff for x being object holds
( x in b₃ iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) );