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 A1: ( ( 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 )
A2: K c= L by A1, CARD_1:3;
A3: M c= N by A1, CARD_1:3;
A4: K +` M = card (K +^ M) by CARD_3:def 1;
A5: L +` N = card (L +^ N) by CARD_3:def 1;
A6: K +^ M c= L +^ N by A2, A3, ORDINAL3:18;
hence K +` M c= L +` N by A4, A5, CARD_1:11; :: thesis: M +` K c= L +` N
thus M +` K c= L +` N by A4, A5, A6, CARD_1:11; :: thesis: verum