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))

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

proof

hence
for x, y being Element of X holds x = (x \ y) * (x \ (x \ y))
; :: thesis: verum
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;(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