:: deftheorem defines the_arity_of MARGREL1:def 10 :
for D being non empty set
for p being Element of relations_on D st p <> empty_rel D holds
for b₃ being Element of NAT holds
( b₃ = the_arity_of p iff for a being FinSequence of D st a in p holds
b₃ = len a );