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