theorem :: HEYTING3:21

for n, k being Element of NAT
for x being set st x in PFBrt ((n + 1),k) holds
ex y being set st
( y in PFBrt (n,k) & y c= x )