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

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