theorem Th87: :: FUNCT_1:88

for Y1, Y2 being set
for f being Function st f " Y1 c= f " Y2 & Y1 c= rng f holds
Y1 c= Y2