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, Lm2, RELAT_1:38; :: thesis: verum