theorem Th27: :: BCIALG_5:27

for i, j, m, n being Nat
for X being BCK-algebra of i,j,m,n st i = min (i,j,m,n) & i = j holds
X is BCK-algebra of i,i,i,i