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