:: deftheorem defines = MARGREL1:def 8 :
for D being non empty set
for p, r being Element of relations_on D holds
( p = r iff for a being FinSequence of D holds
( a in p iff a in r ) );