let A be set ; :: thesis: not A c< {}
assume A1: A c< {} ; :: thesis: contradiction
then A c= {} by XBOOLE_0:def 8;
hence contradiction by A1, Th3; :: thesis: verum