let X be functional with_common_domain set ; :: thesis: ( X = {{} } implies DOM X = {} )
assume A1: X = {{} } ; :: thesis: DOM X = {}
{} in {{} } by TARSKI:def 1;
hence DOM X = {} by A1, Def12, RELAT_1:60; :: thesis: verum