reconsider p = {[ the Element of X, the Element of Y]} as PartFunc of X,Y by RELSET_1:3;
take p ; :: thesis: not p is empty
thus not p is empty ; :: thesis: verum