A2:
On W c= W
by ORDINAL2:7;

{} in On W by ORDINAL3:8;

then reconsider A = 1 as Ordinal of W by A2, Lm3, CLASSES2:5;

A = 1 ;

hence 1 is non empty Ordinal of W by Lm9; :: thesis: verum

{} in On W by ORDINAL3:8;

then reconsider A = 1 as Ordinal of W by A2, Lm3, CLASSES2:5;

A = 1 ;

hence 1 is non empty Ordinal of W by Lm9; :: thesis: verum