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