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