let D be non empty set ; :: thesis: for RD being Equivalence_Relation of D
for F being BinOp of D,RD st F is commutative holds
F /\/ RD is commutative

let RD be Equivalence_Relation of D; :: thesis: for F being BinOp of D,RD st F is commutative holds
F /\/ RD is commutative

let F be BinOp of D,RD; :: thesis: ( F is commutative implies F /\/ RD is commutative )
defpred S1[ Element of Class RD, Element of Class RD] means (F /\/ RD) . (\$1,\$2) = (F /\/ RD) . (\$2,\$1);
assume A1: for a, b being Element of D holds F . (a,b) = F . (b,a) ; :: according to BINOP_1:def 2 :: thesis: F /\/ RD is commutative
A2: now :: thesis: for x1, x2 being Element of D holds S1[ EqClass (RD,x1), EqClass (RD,x2)]
let x1, x2 be Element of D; :: thesis: S1[ EqClass (RD,x1), EqClass (RD,x2)]
(F /\/ RD) . ((EqClass (RD,x1)),(EqClass (RD,x2))) = Class (RD,(F . (x1,x2))) by Th3
.= Class (RD,(F . (x2,x1))) by A1
.= (F /\/ RD) . ((EqClass (RD,x2)),(EqClass (RD,x1))) by Th3 ;
hence S1[ EqClass (RD,x1), EqClass (RD,x2)] ; :: thesis: verum
end;
thus for c1, c2 being Element of Class RD holds S1[c1,c2] from :: according to BINOP_1:def 2 :: thesis: verum