:: deftheorem defines the_arity_of MARGREL1:def 3 :
for p being relation st p <> {} holds
for b₂ being Element of NAT holds
( b₂ = the_arity_of p iff for a being FinSequence st a in p holds
b₂ = len a );