A2: On W c= W by ORDINAL2:9;
{} in On W by ORDINAL3:10;
then reconsider A = 1 as Ordinal of W by A2, Lm3, CLASSES2:6;
A = 1 ;
hence 1 is non empty Ordinal of W ; :: thesis: verum