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 2 :: thesis: (o .:^2) . (x,y) = (o .:^2) . (y,x)
thus (o .:^2) . (x,y) = o .: [:x,y:] by Th44
.= o .: [:y,x:] by A1, Th47
.= (o .:^2) . (y,x) by Th44 ; :: thesis: verum