let D be non empty set ; :: thesis: for o being BinOp of D st o is commutative holds
o .:^2 is commutative
let o be BinOp of D; :: thesis: ( o is commutative implies o .:^2 is commutative )
assume A1: o is commutative ; :: thesis: o .:^2 is commutative
let x, y be Subset of D; :: according to BINOP_1:def 13 :: thesis: (o .:^2 ) . x,y = (o .:^2 ) . y,x
thus (o .:^2 ) . x,y = o .: [:x,y:] by Th45
.= o .: [:y,x:] by A1, Th48
.= (o .:^2 ) . y,x by Th45 ; :: thesis: verum