for X being set
for x being Element of X
for O being Operation of X
for y being Element of X holds
( x,y in O iff y in x . O ) by RELAT_1:169;