theorem :: FUNCT_1:73

for Y being set
for R being Relation st ( for y being object st y in Y holds
R " {y} <> {} ) holds
Y c= rng R