let X be BCK-Algebra_with_Condition(S); :: thesis: for x being Element of X holds (x \ (0. X)) * ((0. X) \ x) = x
for x being Element of X holds (x \ (0. X)) * ((0. X) \ x) = x

proof

let x be Element of X; :: thesis: (x \ (0. X)) * ((0. X) \ x) = x
A1: (0. X) \ x = x `
.= 0. X by BCIALG_1:def 8 ;
x \ (0. X) = x by BCIALG_1:2;
hence (x \ (0. X)) * ((0. X) \ x) = x by A1, Th8; :: thesis: verum

end;

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