:: deftheorem Def9 defines empty_rel MARGREL1:def 9 :
for D being non empty set
for b₂ being Element of relations_on D holds
( b₂ = empty_rel D iff for a being FinSequence of D holds not a in b₂ );