let R be X -valued Relation; :: thesis: R is empty
rng R c= X by Def19;
then rng R = {} by XBOOLE_1:3;
hence R is empty ; :: thesis: verum