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

thus ( X is quasi-associative implies for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) :: thesis: ( ( for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) implies X is quasi-associative )

thus ( X is quasi-associative implies for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) :: thesis: ( ( for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) implies X is quasi-associative )

proof

thus
( ( for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) implies X is quasi-associative )
by Lm18; :: thesis: verum
assume
X is quasi-associative
; :: thesis: for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X

then for x, y being Element of X holds (x `) \ y = (x \ y) ` by Th73;

hence for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X by Lm17; :: thesis: verum

end;then for x, y being Element of X holds (x `) \ y = (x \ y) ` by Th73;

hence for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X by Lm17; :: thesis: verum