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, Th138; :: thesis: exp (M,K) c= exp (N,K)
( M = 0 implies exp (M,K) = 0 ) by A2, Th39;
hence exp (M,K) c= exp (N,K) by A1, Th138; :: thesis: verum