let A be Ordinal; :: thesis: ( A <> {} implies {} in A )
A1: {} c= A ;
assume A <> {} ; :: thesis: {} in A
then {} c< A by A1;
hence {} in A by ORDINAL1:11; :: thesis: verum