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