let a, b be Ordinal; :: thesis: for n being Nat st a in b holds
n *^ (exp (omega,a)) in exp (omega,b)
let n be Nat; :: thesis: ( a in b implies n *^ (exp (omega,a)) in exp (omega,b) )
assume a in b ; :: thesis: n *^ (exp (omega,a)) in exp (omega,b)
then succ a c= b by ORDINAL1:21;
then A1: exp (omega,(succ a)) c= exp (omega,b) by ORDINAL4:27;
A2: exp (omega,(succ a)) = omega *^ (exp (omega,a)) by ORDINAL2:44;
n in omega by ORDINAL1:def 12;
then n *^ (exp (omega,a)) in omega *^ (exp (omega,a)) by ORDINAL3:19, ORDINAL4:22;
hence n *^ (exp (omega,a)) in exp (omega,b) by A1, A2; :: thesis: verum