:: deftheorem defines => WAYBEL_1:def 21 :
for H being non empty RelStr
for a, y being Element of H holds a => y = (a =>) . y;