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 2 :: thesis: o .: [:X,Y:] = o .: [:Y,X:]

now :: thesis: for X, Y being set holds o .: [:X,Y:] c= o .: [:Y,X:]

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 object ; :: 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 object such that
A2: y in dom o and
A3: y in [:X,Y:] and
A4: x = o . y by FUNCT_1:def 6;
reconsider y = y as Element of [:D,D:] by A2;
y = [(y `1),(y `2)] by MCART_1:21;
then ( y `1 in X & y `2 in Y ) by A3, ZFMISC_1:87;
then A5: [(y `2),(y `1)] in [:Y,X:] by ZFMISC_1:87;
A6: ( dom o = [:D,D:] & o . ((y `1),(y `2)) = o . ((y `2),(y `1)) ) by A1, FUNCT_2:def 1;
x = o . ((y `1),(y `2)) by A4, MCART_1:21;
hence x in o .: [:Y,X:] by A6, A5, FUNCT_1:def 6; :: 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