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:] ;
A5: [:K,M:] c= [:L,N:] by A2, A3, ZFMISC_1:96;
hence K *` M c= L *` N by CARD_1:11; :: thesis: M *` K c= L *` N
thus M *` K c= L *` N by A4, A5, CARD_1:11; :: thesis: verum