A1: On W c= W by ORDINAL2:7;
{} in On W by ORDINAL3:8;
then reconsider A = {} as Ordinal of W by A1;
A = {} ;
hence {} is Ordinal of W ; :: thesis: verum