let A be set ; :: thesis: not A c< {}
assume A c< {} ; :: thesis: contradiction
then ( A c= {} & A <> {} ) by XBOOLE_0:def 8;
hence contradiction by Th3; :: thesis: verum