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