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) `

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

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

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

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

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

.= ((x \ y) `) ` by Th9 ;

then (y \ x) ` <= (x \ y) ` by A1;

then A2: ((y \ x) `) \ ((x \ y) `) = 0. X ;

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

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

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

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

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

.= ((y \ x) `) ` by Th9 ;

then (x \ y) ` <= (y \ x) ` by A1;

then ((x \ y) `) \ ((y \ x) `) = 0. X ;

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) `

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

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

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

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

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

.= ((x \ y) `) ` by Th9 ;

then (y \ x) ` <= (x \ y) ` by A1;

then A2: ((y \ x) `) \ ((x \ y) `) = 0. X ;

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

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

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

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

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

.= ((y \ x) `) ` by Th9 ;

then (x \ y) ` <= (y \ x) ` by A1;

then ((x \ y) `) \ ((y \ x) `) = 0. X ;

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