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