let X be BCI-algebra; :: thesis: for a being Element of AtomSet X
for x being Element of BCK-part X holds a \ x = a
let a be Element of AtomSet X; :: thesis: for x being Element of BCK-part X holds a \ x = a
let x be Element of BCK-part X; :: thesis: a \ x = a
a \ (0. X) in { x1 where x1 is Element of X : x1 is atom } by Th33;
then A1: ex x1 being Element of X st
( a \ (0. X) = x1 & x1 is atom ) ;
(a \ x) \ (a \ (0. X)) = (a \ (a \ (0. X))) \ x by Th7;
then (a \ x) \ (a \ (0. X)) = (a \ a) \ x by Th2;
then A2: (a \ x) \ (a \ (0. X)) = x ` by Def5;
x in { x2 where x2 is Element of X : 0. X <= x2 } ;
then ex x2 being Element of X st
( x = x2 & 0. X <= x2 ) ;
then (a \ x) \ (a \ (0. X)) = 0. X by A2;
then a \ x = a \ (0. X) by A1;
hence a \ x = a by Th2; :: thesis: verum