A1: On W c= W by ORDINAL2:7;
{} in On W by CLASSES2:51, ORDINAL3:8;
hence ex b₁ being Element of W st b₁ is ordinal by A1; :: thesis: verum