let X be BCI-algebra; :: thesis: ( ( for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) implies X is quasi-associative )
assume A1: for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ; :: thesis: X is quasi-associative
for x being Element of X holds (x ` ) ` = x `

proof

let x be Element of X; :: thesis: (x ` ) ` = x `
x \ (x ` ) = (x \ (0. X)) \ (x ` ) by Th2;
then x \ (x ` ) in { x2 where x2 is Element of X : 0. X <= x2 } by A1;
then ex x2 being Element of X st
( x \ (x ` ) = x2 & 0. X <= x2 ) ;
then (x \ (x ` )) ` = 0. X by Def11;
then A2: (x ` ) \ ((x ` ) ` ) = 0. X by Th9;
(x ` ) \ x = (x ` ) \ (x \ (0. X)) by Th2;
then (x ` ) \ x in { x1 where x1 is Element of X : 0. X <= x1 } by A1;
then ex x1 being Element of X st
( (x ` ) \ x = x1 & 0. X <= x1 ) ;
then ((x ` ) \ x) ` = 0. X by Def11;
then ((x ` ) ` ) \ (x ` ) = 0. X by Th9;
hence (x ` ) ` = x ` by A2, Def7; :: thesis: verum

end;

hence X is quasi-associative by Def21; :: thesis: verum