:: deftheorem defines relation MARGREL1:def 5 :
for X being set
for b₂ being relation holds
( b₂ is relation of X iff for a being FinSequence st a in b₂ holds
rng a c= X );