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 consider x1 being Element of X such that
A1: ( a \ (0. X) = x1 & x1 is atom ) ;
x in { x2 where x2 is Element of X : 0. X <= x2 } ;
then consider x2 being Element of X such that
A2: ( x = x2 & 0. X <= x2 ) ;
(a \ x) \ (a \ (0. X)) = (a \ (a \ (0. X))) \ x by Th7;
then (a \ x) \ (a \ (0. X)) = (a \ a) \ x by Th2;
then (a \ x) \ (a \ (0. X)) = x ` by Def5;
then (a \ x) \ (a \ (0. X)) = 0. X by A2, Def11;
then a \ x = a \ (0. X) by A1, Def14;
hence a \ x = a by Th2; :: thesis: verum