let X be BCI-algebra; :: thesis: for x, y being Element of BCK-part X holds x \ y in BCK-part X
let x, y be Element of BCK-part X; :: thesis: x \ y in BCK-part X
x in { x1 where x1 is Element of X : 0. X <= x1 } ;
then A1: ex x1 being Element of X st
( x = x1 & 0. X <= x1 ) ;
y in { y1 where y1 is Element of X : 0. X <= y1 } ;
then A2: ex y1 being Element of X st
( y = y1 & 0. X <= y1 ) ;
(x \ y) ` = (x `) \ (y `) by Th9;
then (x \ y) ` = (y `) ` by A1;
then (x \ y) ` = (0. X) ` by A2;
then (x \ y) ` = 0. X by Def5;
then 0. X <= x \ y ;
hence x \ y in BCK-part X ; :: thesis: verum