0_No is No_ordinal ;
hence ex b₁ being uSurreal st b₁ is No_ordinal ; :: thesis: verum