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