dom (disjoin {} ) = {} by Def3, RELAT_1:60;
hence disjoin {} = {} ; :: thesis: verum