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