:: deftheorem Def7 defines relations_on MARGREL1:def 7 :
for D being non empty set
for b₂ being set holds
( b₂ = relations_on D iff for X being set holds
( X in b₂ iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds
len a = len b ) ) ) );