let X be positive-implicative BCK-Algebra_with_Condition(S); :: thesis: for x, y being Element of X holds x = (x \ y) * (x \ (x \ y))
for x, y being Element of X holds x = (x \ y) * (x \ (x \ y))

proof

let x, y be Element of X; :: thesis: x = (x \ y) * (x \ (x \ y))
(x \ y) \ x = (x \ x) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
then x \ y <= x ;
then x = (x \ y) * x by Th45;
hence x = (x \ y) * (x \ (x \ y)) by Th47; :: thesis: verum

end;

hence for x, y being Element of X holds x = (x \ y) * (x \ (x \ y)) ; :: thesis: verum