theorem :: FILTER_1:11

for D being non empty set
for RD being Equivalence_Relation of D
for F, G being BinOp of D,RD st F is_distributive_wrt G holds
F /\/ RD is_distributive_wrt G /\/ RD by Th9, Th10;