for k being Element of NAT
for a being non empty Element of (SubstPoset (NAT,{k})) st a <> {{}} holds
ex f being finite Function st
( f in a & f <> {} )