A1: On W c= W by ORDINAL2:7;
{} in On W by CLASSES2:51, ORDINAL3:8;
then 1 in W by A1, Lm3, CLASSES2:5;
hence not for b₁ being Ordinal of W holds b₁ is empty by Lm9; :: thesis: verum