On W <> {} by CLASSES2:55;
then ( {} in On W & On W c= W ) by ORDINAL2:9, ORDINAL3:10;
then 1 in W by Lm3, CLASSES2:6;
then ( not 1 is empty & 1 is Ordinal of W ) by Def2;
hence not for b₁ being Ordinal of W holds b₁ is empty ; :: thesis: verum