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