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) `
(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 A2: ((x \ y) ` ) \ ((y \ x) ` ) = 0. X by Def11;
(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 ((y \ x) ` ) \ ((x \ y) ` ) = 0. X by Def11;
hence (x \ y) ` = (y \ x) ` by A2, Def7; :: thesis: verum