On W <> {} by CLASSES2:55;
then ( {} in On W & On W c= W ) by ORDINAL2:9, ORDINAL3:10;
then 1 in W by Lm3, CLASSES2:6;
then reconsider A = 1 as Ordinal of W by Def2;
A = 1 ;
hence 1 is non empty Ordinal of W ; :: thesis: verum