( dom (R | X) c= dom R & dom R c= A ) by Def16, Th51;
hence dom (R | X) c= A ; :: according to RELAT_1:def 18 :: thesis: R | X is X -defined
thus dom (R | X) c= X by Th51; :: according to RELAT_1:def 18 :: thesis: verum