disjoin {} = {} by Def3, RELAT_1:38;