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