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

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