let f be Relation of X,Y; :: thesis: not f is total
assume f is total ; :: thesis: contradiction
then dom f = X by Def2;
hence contradiction ; :: thesis: verum