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