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