( [:{} ,{} :] = {} & dom {} = {} ) by ZFMISC_1:113;
then dom (~ {} ) = {} by FUNCT_4:47;
hence ~ {} = {} ; :: thesis: verum