let X be BCI-algebra; :: thesis: ( X is BCI-algebra of 0 , 0 , 0 , 0 iff X is BCK-algebra of 0 , 0 , 0 , 0 )

thus ( X is BCI-algebra of 0 , 0 , 0 , 0 implies X is BCK-algebra of 0 , 0 , 0 , 0 ) :: thesis: ( X is BCK-algebra of 0 , 0 , 0 , 0 implies X is BCI-algebra of 0 , 0 , 0 , 0 )

thus ( X is BCI-algebra of 0 , 0 , 0 , 0 implies X is BCK-algebra of 0 , 0 , 0 , 0 ) :: thesis: ( X is BCK-algebra of 0 , 0 , 0 , 0 implies X is BCI-algebra of 0 , 0 , 0 , 0 )

proof

thus
( X is BCK-algebra of 0 , 0 , 0 , 0 implies X is BCI-algebra of 0 , 0 , 0 , 0 )
; :: thesis: verum
assume A1:
X is BCI-algebra of 0 , 0 , 0 , 0
; :: thesis: X is BCK-algebra of 0 , 0 , 0 , 0

then X is BCI-algebra of 0 , 0 ,0 + 0,0 + 0 ;

then reconsider X = X as BCK-algebra by Th36;

for x, y being Element of X holds Polynom (0,0,x,y) = Polynom (0,0,y,x) by A1, Def3;

hence X is BCK-algebra of 0 , 0 , 0 , 0 by Def3; :: thesis: verum

end;then X is BCI-algebra of 0 , 0 ,0 + 0,0 + 0 ;

then reconsider X = X as BCK-algebra by Th36;

for x, y being Element of X holds Polynom (0,0,x,y) = Polynom (0,0,y,x) by A1, Def3;

hence X is BCK-algebra of 0 , 0 , 0 , 0 by Def3; :: thesis: verum