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

for x being Element of X holds (x \ (0. X)) * ((0. X) \ x) = x

proof

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