let X be BCI-algebra; :: thesis: for x, y being Element of X st x \ y = 0. X holds

(y \ x) ` = 0. X

let x, y be Element of X; :: thesis: ( x \ y = 0. X implies (y \ x) ` = 0. X )

assume x \ y = 0. X ; :: thesis: (y \ x) ` = 0. X

then (x \ x) \ (y \ x) = 0. X by Th4;

hence (y \ x) ` = 0. X by Def5; :: thesis: verum

(y \ x) ` = 0. X

let x, y be Element of X; :: thesis: ( x \ y = 0. X implies (y \ x) ` = 0. X )

assume x \ y = 0. X ; :: thesis: (y \ x) ` = 0. X

then (x \ x) \ (y \ x) = 0. X by Th4;

hence (y \ x) ` = 0. X by Def5; :: thesis: verum