A1: alpha + beta = [(((L_ alpha) ++ {beta}) \/ ({alpha} ++ (L_ beta))),(((R_ alpha) ++ {beta}) \/ ({alpha} ++ (R_ beta)))] by SURREALR:28;
( R_ alpha = {} & {} = R_ beta ) by Def10;
then ( (R_ alpha) ++ {beta} = {} & {} = {alpha} ++ (R_ beta) ) by SURREALR:27;
hence alpha + beta is No_ordinal by A1; :: thesis: verum