let K, L, M, N be Cardinal; :: thesis: ( ( ( K in L & M in N ) or ( K c= L & M in N ) or ( K in L & M c= N ) or ( K c= L & M c= N ) ) implies ( K +` M c= L +` N & M +` K c= L +` N ) )
assume ( ( K in L & M in N ) or ( K c= L & M in N ) or ( K in L & M c= N ) or ( K c= L & M c= N ) ) ; :: thesis: ( K +` M c= L +` N & M +` K c= L +` N )
then ( K c= L & M c= N & K = K & L = L & M = M & N = N ) by CARD_1:13;
then A1: ( K +` M = card (K +^ M) & L +` N = card (L +^ N) & K +^ M c= L +^ N ) by CARD_2:def 1, ORDINAL3:21;
hence K +` M c= L +` N by CARD_1:27; :: thesis: M +` K c= L +` N
thus M +` K c= L +` N by A1, CARD_1:27; :: thesis: verum