:: deftheorem defines meet FUNCT_6:def 4 :
for f being Function holds meet f = meet (rng f);