:: deftheorem Def14 defines NatMinor PRE_POLY:def 15 :
for X being set
for f being Function of X,NAT
for b₃ being Subset of (Funcs (X,NAT)) holds
( b₃ = NatMinor f iff for g being natural-valued ManySortedSet of X holds
( g in b₃ iff for x being set st x in X holds
g . x <= f . x ) );