On W <> {} by CLASSES2:55;
then ( {} in On W & On W c= W ) by ORDINAL2:9, ORDINAL3:10;
hence ex b₁ being Ordinal st b₁ in W ; :: thesis: verum