let X, Y be set ; :: thesis: for D being non empty set
for o being BinOp of D st o is commutative holds
o .: [:X,Y:] = o .: [:Y,X:]
let D be non empty set ; :: thesis: for o being BinOp of D st o is commutative holds
o .: [:X,Y:] = o .: [:Y,X:]
let o be BinOp of D; :: thesis: ( o is commutative implies o .: [:X,Y:] = o .: [:Y,X:] )
assume A1: for a, b being Element of D holds o . a,b = o . b,a ; :: according to BINOP_1:def 13 :: thesis: o .: [:X,Y:] = o .: [:Y,X:]

now

let X, Y be set ; :: thesis: o .: [:X,Y:] c= o .: [:Y,X:]
thus o .: [:X,Y:] c= o .: [:Y,X:] :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in o .: [:X,Y:] or x in o .: [:Y,X:] )
assume x in o .: [:X,Y:] ; :: thesis: x in o .: [:Y,X:]
then consider y being set such that
A2: ( y in dom o & y in [:X,Y:] & x = o . y ) by FUNCT_1:def 12;
A3: dom o = [:D,D:] by FUNCT_2:def 1;
reconsider y = y as Element of [:D,D:] by A2;
y = [(y `1 ),(y `2 )] by MCART_1:23;
then ( y `1 in X & y `2 in Y & x = o . (y `1 ),(y `2 ) & o . (y `1 ),(y `2 ) = o . (y `2 ),(y `1 ) ) by A1, A2, ZFMISC_1:106;
then ( [(y `2 ),(y `1 )] in [:D,D:] & [(y `2 ),(y `1 )] in [:Y,X:] & x = o . [(y `2 ),(y `1 )] ) by ZFMISC_1:106;
hence x in o .: [:Y,X:] by A3, FUNCT_1:def 12; :: thesis: verum

end;

end;

hence ( o .: [:X,Y:] c= o .: [:Y,X:] & o .: [:Y,X:] c= o .: [:X,Y:] ) ; :: according to XBOOLE_0:def 10 :: thesis: verum