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