let i, j, m, n be Element of NAT ; :: thesis: for X being BCK-algebra of i,j,m,n holds X is BCK-algebra of i,j,j,n
let X be BCK-algebra of i,j,m,n; :: thesis: X is BCK-algebra of i,j,j,n
for x, y being Element of X holds Polynom i,j,x,y = Polynom j,n,y,x
proof
let x,
y be
Element of
X;
:: thesis: Polynom i,j,x,y = Polynom j,n,y,x
Polynom i,
j,
x,
y = Polynom m,
n,
y,
x
by Def2;
hence
Polynom i,
j,
x,
y = Polynom j,
n,
y,
x
by Th8;
:: thesis: verum
end;
hence
X is BCK-algebra of i,j,j,n
by Def2; :: thesis: verum