let M, N, K be Cardinal; :: thesis: ( ( 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 ) )
assume that
A1: ( M in N or M c= N ) and
A2: K <> 0 ; :: thesis: ( exp K,M c= exp K,N & exp M,K c= exp N,K )
thus exp K,M c= exp K,N by A1, A2, Th70; :: thesis: exp M,K c= exp N,K
( M = 0 implies exp M,K = 0 ) by A2, CARD_2:39;
hence exp M,K c= exp N,K by A1, Th70; :: thesis: verum