theorem Th35: :: HEYTING3:35

for k being Element of NAT
for a being Element of (SubstPoset (NAT,{k}))
for a9 being Element of Fin (PFuncs (NAT,{k}))
for B being non empty finite Subset of NAT st B = Involved a9 & a9 = a holds
for X being set st X in a holds
for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X