set A = { (dom f) where f is Element of X : verum } ;
A1: { (dom f) where f is Element of X : verum } c= {{}}

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (dom f) where f is Element of X : verum } or e in {{}} )
assume e in { (dom f) where f is Element of X : verum } ; :: thesis: e in {{}}
then ex f being Element of X st e = dom f ;
then e = dom {} by SUBSET_1:def 1;
hence e in {{}} by TARSKI:def 1; :: thesis: verum

end;

{{}} c= { (dom f) where f is Element of X : verum }

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in {{}} or e in { (dom f) where f is Element of X : verum } )
assume e in {{}} ; :: thesis: e in { (dom f) where f is Element of X : verum }
then e = {} by TARSKI:def 1;
then e = dom {} ;
then e = dom the Element of X by SUBSET_1:def 1;
hence e in { (dom f) where f is Element of X : verum } ; :: thesis: verum

end;

then { (dom f) where f is Element of X : verum } = {{}} by A1;
hence DOM X is empty by SETFAM_1:10; :: thesis: verum