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