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 ` ) \ (x \ (0. X)) by Th2;
then (x ` ) \ x in { x1 where x1 is Element of X : 0. X <= x1 } by A1;
then consider x1 being Element of X such that
A2: ( (x ` ) \ x = x1 & 0. X <= x1 ) ;
((x ` ) \ x) ` = 0. X by A2, Def11;
then A3: ((x ` ) ` ) \ (x ` ) = 0. X by Th9;
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 consider x2 being Element of X such that
A4: ( x \ (x ` ) = x2 & 0. X <= x2 ) ;
(x \ (x ` )) ` = 0. X by A4, Def11;
then (x ` ) \ ((x ` ) ` ) = 0. X by Th9;
hence (x ` ) ` = x ` by A3, Def7; :: thesis: verum

end;

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