:: deftheorem Def4 defines /\/ FILTER_1:def 4 :
for D being non empty set
for R being Equivalence_Relation of D
for b being BinOp of D st b is BinOp of D,R holds
for b₄ being BinOp of (Class R) holds
( b₄ = b /\/ R iff for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b₄ . (x,y) = Class (R,(b . (x1,y1))) );