:: deftheorem defines inf SUPINF_2:def 2 :
for D being ext-real-membered set
for X being set
for Y being Subset of D
for F being PartFunc of X,Y holds inf F = inf (rng F);