let X be BCI-algebra; :: thesis: ( ( for x being Element of X holds x ` = x ) implies for x, y being Element of X holds x \ y = y \ x )

assume A1: for x being Element of X holds x ` = x ; :: thesis: for x, y being Element of X holds x \ y = y \ x

let x, y be Element of X; :: thesis: x \ y = y \ x

A2: (y \ x) \ (x \ y) = ((y `) \ x) \ (x \ y) by A1

.= ((y `) \ (x `)) \ (x \ y) by A1

.= 0. X by Th1 ;

(x \ y) \ (y \ x) = ((x `) \ y) \ (y \ x) by A1

.= ((x `) \ (y `)) \ (y \ x) by A1

.= 0. X by Th1 ;

hence x \ y = y \ x by A2, Def7; :: thesis: verum

assume A1: for x being Element of X holds x ` = x ; :: thesis: for x, y being Element of X holds x \ y = y \ x

let x, y be Element of X; :: thesis: x \ y = y \ x

A2: (y \ x) \ (x \ y) = ((y `) \ x) \ (x \ y) by A1

.= ((y `) \ (x `)) \ (x \ y) by A1

.= 0. X by Th1 ;

(x \ y) \ (y \ x) = ((x `) \ y) \ (y \ x) by A1

.= ((x `) \ (y `)) \ (y \ x) by A1

.= 0. X by Th1 ;

hence x \ y = y \ x by A2, Def7; :: thesis: verum