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

per cases ( N is finite or not N is finite ) ;

suppose A5: 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, A5, CARD_3:92;
A6: card (Segm K) = K ;
A7: card (Segm L) = L ;
A8: card (Segm M) = M ;
A9: card (Segm N) = N ;
A10: K +` M = card (Segm ((card K) + (card M))) by Th37;
A11: L +` N = card (Segm ((card L) + (card N))) by Th37;
A12: card K < card L by A2, A6, A7, NAT_1:41;
card M < card N by A3, A8, A9, NAT_1:41;
then (card K) + (card M) < (card L) + (card N) by A12, XREAL_1:8;
hence K +` M in L +` N by A10, A11, NAT_1:41; :: thesis: verum

end;

suppose A13: not N is finite ; :: thesis: K +` M in L +` N

then A14: L +` N = N by A4, Th75;
A15: omega c= N by A13, 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 A16: ( ( K is finite & M is finite ) or K +` M = M or ( K +` M = K & K in N ) ) by A2, A4, Th75;
( K is finite & M is finite implies K +` M in L +` N ) by A14, A15, CARD_1:61;
hence K +` M in L +` N by A3, A4, A13, A16, Th75; :: thesis: verum

end;

end;

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