let X, Y be set ; :: thesis: {} is Relation of X,Y
{} c= [:X,Y:] by XBOOLE_1:2;
hence {} is Relation of X,Y by Def1; :: thesis: verum