let X be commutative BCK-algebra; :: thesis: ( X is BCI-commutative BCI-algebra & X is BCI-weakly-commutative BCI-algebra )
A1: for x, y being Element of X holds (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x)
proof
let x, y be Element of X; :: thesis: (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x)
A2: (0. X) \ (x \ y) = (x \ y) `
.= 0. X by BCIALG_1:def 8 ;
x \ (x \ y) = y \ (y \ x) by Def1;
hence (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x) by A2, BCIALG_1:2; :: thesis: verum
end;
for x, y being Element of X st x \ y = 0. X holds
x = y \ (y \ x) by BCIALG_1:def 11, Th5;
hence ( X is BCI-commutative BCI-algebra & X is BCI-weakly-commutative BCI-algebra ) by A1, Def4, Def5; :: thesis: verum