let X, Y be set ; :: thesis: <:{} ,X,Y:> = {}
( dom {} c= X & rng {} c= Y ) by XBOOLE_1:2;
hence <:{} ,X,Y:> = {} by Th85; :: thesis: verum