theorem :: MARGREL1:3

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