let a, b be Ordinal; :: thesis: ( 1 in a & a in b implies b +^ a in a *^ b )
assume A1: ( 1 in a & a in b ) ; :: thesis: b +^ a in a *^ b
then A2: 2 *^ b c= a *^ b by Lm2, ORDINAL1:21, ORDINAL2:41;
b +^ a in b +^ b by A1, ORDINAL2:32;
then b +^ a in 2 *^ b by Th2;
hence b +^ a in a *^ b by A2; :: thesis: verum