let i, j, k, l, m, n be Nat; :: thesis: 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; :: thesis: ( l >= j & k >= n implies X is BCK-algebra of k,l,l,k )

assume that

A1: l >= j and

A2: k >= n ; :: thesis: 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; :: thesis: verum

X is BCK-algebra of k,l,l,k

let X be BCK-algebra of i,j,m,n; :: thesis: ( l >= j & k >= n implies X is BCK-algebra of k,l,l,k )

assume that

A1: l >= j and

A2: k >= n ; :: thesis: 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; :: thesis: verum