:: deftheorem defines = MARGREL1:def 2 :
for p, r being relation holds
( p = r iff for a being FinSequence holds
( a in p iff a in r ) );