:: deftheorem defines inclusion WAYBEL_1:def 17 :
for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds inclusion g = id (Image g);