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
A1: ( x in { x1 where x1 is Element of X : 0. X <= x1 } & y in { y1 where y1 is Element of X : 0. X <= y1 } ) ;
then consider x1 being Element of X such that
A2: ( x = x1 & 0. X <= x1 ) ;
consider y1 being Element of X such that
A3: ( y = y1 & 0. X <= y1 ) by A1;
(x \ y) ` = (x ` ) \ (y ` ) by Th9;
then (x \ y) ` = (y ` ) ` by A2, Def11;
then (x \ y) ` = (0. X) ` by A3, Def11;
then (x \ y) ` = 0. X by Def5;
then 0. X <= x \ y by Def11;
hence x \ y in BCK-part X ; :: thesis: verum