let f be Relation of X,Y; :: thesis: not f is total
assume f is total ; :: thesis: contradiction
then ( dom f = X & f = {} ) by Def4;
hence contradiction ; :: thesis: verum