:: deftheorem defines relation MARGREL1:def 6 :
for X being set
for k being Element of NAT
for b₃ being relation holds
( b₃ is relation of X,k iff ( b₃ is relation of X & b₃ is relation_length of k ) );