let i, j, m, n, k be Element of NAT ; :: thesis: for X being BCK-algebra of i,j,m,n st k >= max i,j,m,n holds
X is BCK-algebra of k,k,k,k
let X be BCK-algebra of i,j,m,n; :: thesis: ( k >= max i,j,m,n implies X is BCK-algebra of k,k,k,k )
X is BCK-algebra of n,j,m,n by Th10;
then A1: X is BCK-algebra of n,j,j,n by Th9;
assume A1a: k >= max i,j,m,n ; :: thesis: X is BCK-algebra of k,k,k,k
A2: ( max i,j,m,n >= j & max i,j,m,n >= n ) by Th12b;
then B3: k - j is Element of NAT by A1a, NAT_1:21, XXREAL_0:2;
consider t being Element of NAT such that
B3a: t = k - j by B3;
B4: k - n is Element of NAT by A2, A1a, NAT_1:21, XXREAL_0:2;
consider t1 being Element of NAT such that
B4a: t1 = k - n by B4;
X is BCK-algebra of n + t1,j,j,n + t1 by A1, Th5b;
then X is BCK-algebra of k,j + t,j + t,k by B4a, Th6b;
hence X is BCK-algebra of k,k,k,k by B3a; :: thesis: verum