theorem Th21: :: FUNCT_6:25

for f being Function st f <> {} holds
for x being object holds
( x in meet f iff for y being object st y in dom f holds
x in f . y )