for p being relation st ( for a being FinSequence holds not a in p ) holds
p = {} ;