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 S₁[ 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 13 :: thesis: F /\/ RD is commutative

A2: now

let x1, x2 be Element of D; :: thesis: S₁[ 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 S₁[ EqClass RD,x1, EqClass RD,x2] ; :: thesis: verum

end;

thus for c1, c2 being Element of Class RD holds S₁[c1,c2] from FILTER_1:sch 2(A2); :: according to BINOP_1:def 13 :: thesis: verum