theorem :: WAYBEL15:12

for L1, L2 being non empty RelStr
for f being Function of L1,L2
for X being Subset of (Image f) holds (inclusion f) .: X = X by FUNCT_1:92;