let D be non empty set ; :: thesis: 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
let RD be Equivalence_Relation of D; :: thesis: for F, G being BinOp of D,RD st F is_distributive_wrt G holds
F /\/ RD is_distributive_wrt G /\/ RD
let F, G be BinOp of D,RD; :: thesis: ( F is_distributive_wrt G implies F /\/ RD is_distributive_wrt G /\/ RD )
assume that
A1: F is_left_distributive_wrt G and
A2: F is_right_distributive_wrt G ; :: according to BINOP_1:def 11 :: thesis: F /\/ RD is_distributive_wrt G /\/ RD
thus ( F /\/ RD is_left_distributive_wrt G /\/ RD & F /\/ RD is_right_distributive_wrt G /\/ RD ) by A1, A2, Th9, Th10; :: according to BINOP_1:def 11 :: thesis: verum