let x be Element of X; :: thesis: x is DOM X -defined
DOM X = dom x by CARD_3:108;
hence x is DOM X -defined by RELAT_1:def 18; :: thesis: verum