( R_ alpha = {} & {} = R_ beta ) by Def10;
then A2: alpha * beta = [((comp ((L_ alpha),alpha,beta,(L_ beta))) \/ (comp ((R_ alpha),alpha,beta,{}))),((comp ((L_ alpha),alpha,beta,{})) \/ (comp ({},alpha,beta,(L_ beta))))] by SURREALR:50;
comp ({},alpha,beta,(L_ beta)) = comp ((L_ beta),beta,alpha,{}) by SURREALR:53;
then ( comp ({},alpha,beta,(L_ beta)) = {} & {} = comp ((L_ alpha),alpha,beta,{}) ) by SURREALR:49;
hence alpha * beta is No_ordinal by A2; :: thesis: verum