let i, j, k, l, m, n be Nat; for X being BCK-algebra of i,j,m,n st l >= j & k >= n holds
X is BCK-algebra of k,l,l,k
let X be BCK-algebra of i,j,m,n; ( l >= j & k >= n implies X is BCK-algebra of k,l,l,k )
assume that
A1:
l >= j
and
A2:
k >= n
; X is BCK-algebra of k,l,l,k
l - j is Element of NAT
by A1, NAT_1:21;
then consider t being Element of NAT such that
A3:
t = l - j
;
k - n is Element of NAT
by A2, NAT_1:21;
then consider t1 being Element of NAT such that
A4:
t1 = k - n
;
X is BCK-algebra of n,j,m,n
by Th22;
then
X is BCK-algebra of n,j,j,n
by Th21;
then
X is BCK-algebra of n + t1,j,j,n + t1
by Th17;
then
X is BCK-algebra of k,j + t,j + t,k
by A4, Th18;
hence
X is BCK-algebra of k,l,l,k
by A3; verum