:: deftheorem Def2 defines BinOp FILTER_1:def 2 :
for D being non empty set
for R being Relation
for b₃ being BinOp of D holds
( b₃ is BinOp of D,R iff for x1, y1, x2, y2 being Element of D st [x1,y1] in R & [x2,y2] in R holds
[(b₃ . (x1,x2)),(b₃ . (y1,y2))] in R );