x .--> y = {[x,y]} by FUNCT_4:87;
hence x .--> y is trivial ; :: thesis: verum