let X be set ; :: thesis: 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 )
let x be Element of X; :: thesis: for O being Operation of X
for y being Element of X holds
( x,y in O iff y in x . O )
let O be Operation of X; :: thesis: for y being Element of X holds
( x,y in O iff y in x . O )
let y be Element of X; :: thesis: ( x,y in O iff y in x . O )
( x,y in O iff [x,y] in O ) by Def1;
hence ( x,y in O iff y in x . O ) by RELAT_1:169; :: thesis: verum