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

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