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