let R be X -defined Relation; :: thesis: R is empty
dom R c= X by Def16;
hence R is empty by XBOOLE_1:3; :: thesis: verum