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

thus ( X is quasi-associative implies for x being Element of X holds x ` <= x ) :: thesis: ( ( for x being Element of X holds x ` <= x ) implies X is quasi-associative )

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

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

then for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X by Lm17;

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

thus ( X is quasi-associative implies for x being Element of X holds x ` <= x ) :: thesis: ( ( for x being Element of X holds x ` <= x ) implies X is quasi-associative )

proof

assume
for x being Element of X holds x ` <= x
; :: thesis: X is quasi-associative
assume A1:
X is quasi-associative
; :: thesis: for x being Element of X holds x ` <= x

let x be Element of X; :: thesis: x ` <= x

((x `) `) \ x = 0. X by Th1;

then (x `) \ x = 0. X by A1;

hence x ` <= x ; :: thesis: verum

end;let x be Element of X; :: thesis: x ` <= x

((x `) `) \ x = 0. X by Th1;

then (x `) \ x = 0. X by A1;

hence x ` <= x ; :: thesis: verum

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

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

then for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X by Lm17;

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