theorem :: CARD_2:93

for K, M, N being Cardinal holds
( ( not M in N & not M c= N ) or K = 0 or ( exp (K,M) c= exp (K,N) & exp (M,K) c= exp (N,K) ) )