( {} in On W & On W c= W ) by ORDINAL2:9, ORDINAL3:10;
then reconsider A = {} as Ordinal of W ;
A = {} ;
hence {} is Ordinal of W ; :: thesis: verum