let X be BCK-algebra; :: thesis: ( X is commutative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) )

thus ( X is commutative BCK-algebra implies for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) :: thesis: ( ( for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) implies X is commutative BCK-algebra )

for x, y being Element of X holds x \ (x \ y) = y \ (y \ x)

thus ( X is commutative BCK-algebra implies for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) :: thesis: ( ( for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) implies X is commutative BCK-algebra )

proof

assume A2:
for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x)
; :: thesis: X is commutative BCK-algebra
assume A1:
X is commutative BCK-algebra
; :: thesis: for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x)

let x, y be Element of X; :: thesis: x \ (x \ y) <= y \ (y \ x)

x \ (x \ y) = y \ (y \ x) by A1, Def1;

then (x \ (x \ y)) \ (y \ (y \ x)) = 0. X by BCIALG_1:def 5;

hence x \ (x \ y) <= y \ (y \ x) ; :: thesis: verum

end;let x, y be Element of X; :: thesis: x \ (x \ y) <= y \ (y \ x)

x \ (x \ y) = y \ (y \ x) by A1, Def1;

then (x \ (x \ y)) \ (y \ (y \ x)) = 0. X by BCIALG_1:def 5;

hence x \ (x \ y) <= y \ (y \ x) ; :: thesis: verum

for x, y being Element of X holds x \ (x \ y) = y \ (y \ x)

proof

hence
X is commutative BCK-algebra
by Def1; :: thesis: verum
let x, y be Element of X; :: thesis: x \ (x \ y) = y \ (y \ x)

y \ (y \ x) <= x \ (x \ y) by A2;

then A3: (y \ (y \ x)) \ (x \ (x \ y)) = 0. X ;

x \ (x \ y) <= y \ (y \ x) by A2;

then (x \ (x \ y)) \ (y \ (y \ x)) = 0. X ;

hence x \ (x \ y) = y \ (y \ x) by A3, BCIALG_1:def 7; :: thesis: verum

end;y \ (y \ x) <= x \ (x \ y) by A2;

then A3: (y \ (y \ x)) \ (x \ (x \ y)) = 0. X ;

x \ (x \ y) <= y \ (y \ x) by A2;

then (x \ (x \ y)) \ (y \ (y \ x)) = 0. X ;

hence x \ (x \ y) = y \ (y \ x) by A3, BCIALG_1:def 7; :: thesis: verum