let G be Group; :: thesis: for a, b being Element of G holds
( a |^ b = a iff a * b = b * a )
let a, b be Element of G; :: thesis: ( a |^ b = a iff a * b = b * a )
thus ( a |^ b = a implies a * b = b * a ) :: thesis: ( a * b = b * a implies a |^ b = a )

proof

assume a |^ b = a ; :: thesis: a * b = b * a
then a = (b ") * (a * b) by GROUP_1:def 3;
hence a * b = b * a by GROUP_1:13; :: thesis: verum

end;

assume a * b = b * a ; :: thesis: a |^ b = a
then a = (b ") * (a * b) by GROUP_1:13;
hence a |^ b = a by GROUP_1:def 3; :: thesis: verum