theorem :: CARD_3:3

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