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