let U be Universe; :: thesis: ( On U <> {} & On U is limit_ordinal )
card U = On U by Th9;
hence ( On U <> {} & On U is limit_ordinal ) by Th19; :: thesis: verum