let X be non empty BCIStr_1 ; :: thesis: ( 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 ) ) ; :: thesis: X is BCI-Algebra_with_Condition(S)

for x, y, z being Element of X holds (x \ y) \ z = x \ (y * z)

( (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 ) ) ; :: thesis: X is BCI-Algebra_with_Condition(S)

for x, y, z being Element of X holds (x \ y) \ z = x \ (y * z)

proof

hence
X is BCI-Algebra_with_Condition(S)
by A1, Def2; :: thesis: verum
let x, y, z be Element of X; :: thesis: (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; :: thesis: verum

end;(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; :: thesis: verum