let i, j, k, m, n be 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 )
assume A1: k >= max (i,j,m,n) ; :: thesis: X is BCK-algebra of k,k,k,k
max (i,j,m,n) >= n by Th26;
then k - n is Element of NAT by A1, NAT_1:21, XXREAL_0:2;
then consider t1 being Element of NAT such that
A2: t1 = k - n ;
max (i,j,m,n) >= j by Th26;
then k - j is Element of NAT by A1, NAT_1:21, XXREAL_0:2;
then consider t being Element of NAT such that
A3: t = k - j ;
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 A2, Th18;
hence X is BCK-algebra of k,k,k,k by A3; :: thesis: verum