let X be non empty BCIStr_1 ; ( X is BCI-algebra & ( for x, y being Element of X holds
( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) ) ) implies X is BCI-Algebra_with_Condition(S) )
assume that
A1:
X is BCI-algebra
and
A2:
for x, y being Element of X holds
( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds
t <= x * y ) )
; X is BCI-Algebra_with_Condition(S)
for x, y, z being Element of X holds (x \ y) \ z = x \ (y * z)
proof
let x,
y,
z be
Element of
X;
(x \ y) \ z = x \ (y * z)
(y * z) \ y <= z
by A2;
then A3:
((y * z) \ y) \ z = 0. X
;
(x \ ((x \ y) \ z)) \ y =
(x \ y) \ ((x \ y) \ z)
by A1, BCIALG_1:7
.=
((x \ y) \ (0. X)) \ ((x \ y) \ z)
by A1, BCIALG_1:2
;
then
((x \ ((x \ y) \ z)) \ y) \ (z \ (0. X)) = 0. X
by A1, BCIALG_1:11;
then
(x \ ((x \ y) \ z)) \ y <= z \ (0. X)
;
then
(x \ ((x \ y) \ z)) \ y <= z
by A1, BCIALG_1:2;
then
x \ ((x \ y) \ z) <= y * z
by A2;
then
(x \ ((x \ y) \ z)) \ (y * z) = 0. X
;
then A4:
(x \ (y * z)) \ ((x \ y) \ z) = 0. X
by A1, BCIALG_1:7;
((x \ y) \ (x \ (y * z))) \ ((y * z) \ y) = 0. X
by A1, BCIALG_1:11;
then
((x \ y) \ (x \ (y * z))) \ z = 0. X
by A1, A3, BCIALG_1:3;
then
((x \ y) \ z) \ (x \ (y * z)) = 0. X
by A1, BCIALG_1:7;
hence
(x \ y) \ z = x \ (y * z)
by A1, A4, BCIALG_1:def 7;
verum
end;
hence
X is BCI-Algebra_with_Condition(S)
by A1, Def2; verum