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

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