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

thus ( X is quasi-associative implies for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) :: thesis: ( ( for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) implies X is quasi-associative )

then for x being Element of X holds x ` <= x by Lm19;

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

thus ( X is quasi-associative implies for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) :: thesis: ( ( for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) implies X is quasi-associative )

proof

assume
for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z)
; :: thesis: X is quasi-associative
assume
X is quasi-associative
; :: thesis: for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z)

then for x being Element of X holds x ` <= x by Th71;

hence for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) by Lm19; :: thesis: verum

end;then for x being Element of X holds x ` <= x by Th71;

hence for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) by Lm19; :: thesis: verum

then for x being Element of X holds x ` <= x by Lm19;

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