let K, L, M, N be Cardinal; :: thesis: ( K in L & M in N implies ( K +` M in L +` N & M +` K in L +` N ) )
A1: for K, L, M, N being Cardinal st K in L & M in N & L c= N holds
K +` M in L +` N

proof

let K, L, M, N be Cardinal; :: thesis: ( K in L & M in N & L c= N implies K +` M in L +` N )
assume that
A2: K in L and
A3: M in N and
A4: L c= N ; :: thesis: K +` M in L +` N

A5: now

assume A6: N is finite ; :: thesis: K +` M in L +` N
then reconsider N = N as finite Cardinal ;
reconsider L = L, M = M, K = K as finite Cardinal by A2, A3, A4, A6, CARD_3:92;
A7: card K = K by CARD_1:def 2;
A8: card L = L by CARD_1:def 2;
A9: card M = M by CARD_1:def 2;
A10: card N = N by CARD_1:def 2;
A11: K +` M = card ((card K) + (card M)) by A7, A9, Th51;
A12: L +` N = card ((card L) + (card N)) by A8, A10, Th51;
A13: card K < card L by A2, A7, A8, NAT_1:41;
card M < card N by A3, A9, A10, NAT_1:41;
then (card K) + (card M) < (card L) + (card N) by A13, XREAL_1:8;
hence K +` M in L +` N by A11, A12, NAT_1:41; :: thesis: verum

end;

now

assume A14: not N is finite ; :: thesis: K +` M in L +` N
then A15: L +` N = N by A4, Th118;
A16: omega c= N by A14, CARD_3:85;
( ( K c= M & ( M is finite or not M is finite ) ) or ( M c= K & ( K is finite or not K is finite ) ) ) ;
then A17: ( ( K is finite & M is finite ) or K +` M = M or ( K +` M = K & K in N ) ) by A2, A4, Th118;

now

assume that
A18: K is finite and
A19: M is finite ; :: thesis: K +` M in L +` N
reconsider K = K, M = M as finite Cardinal by A18, A19;
A20: card K = K by CARD_1:def 2;
card M = M by CARD_1:def 2;
then K +` M = card ((card K) + (card M)) by A20, Th51
.= (card K) + (card M) by CARD_1:def 2 ;
hence K +` M in L +` N by A15, A16, TARSKI:def 3; :: thesis: verum

end;

hence K +` M in L +` N by A3, A4, A14, A17, Th118; :: thesis: verum

end;

hence K +` M in L +` N by A5; :: thesis: verum

end;

( L c= N or N c= L ) ;
hence ( K in L & M in N implies ( K +` M in L +` N & M +` K in L +` N ) ) by A1; :: thesis: verum