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