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