:: deftheorem defines relation_length MARGREL1:def 4 :
for k being Element of NAT
for b₂ being relation holds
( b₂ is relation_length of k iff for a being FinSequence st a in b₂ holds
len a = k );