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 ) 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 2, ZFMISC_1:119;
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