let X be non empty BCIStr_0 ; ( X is associative BCI-algebra iff for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) )
thus
( X is associative BCI-algebra implies for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) )
( ( for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) implies X is associative BCI-algebra )proof
assume A1:
X is
associative BCI-algebra
;
for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x )
let x,
y,
z be
Element of
X;
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x )
(z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (y \ x)) \ (z \ x)
by A1, Def20;
then
(z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (z \ x)) \ (y \ x)
by A1, Th7;
then
(z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (z \ x)) \ (x \ y)
by A1, Th48;
then A2:
(z \ y) \ ((y \ x) \ (z \ x)) = 0. X
by A1, Th1;
((y \ x) \ (z \ x)) \ (z \ y) = ((y \ x) \ (z \ x)) \ (y \ z)
by A1, Th48;
then
((y \ x) \ (z \ x)) \ (z \ y) = 0. X
by A1, Def3;
hence
(
(y \ x) \ (z \ x) = z \ y &
x \ (0. X) = x )
by A1, A2, Def7, Th2;
verum
end;
thus
( ( for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) implies X is associative BCI-algebra )
verum