:: deftheorem Def1 defines RelIncl WELLORD2:def 1 :
for X being set
for b₂ being Relation holds
( b₂ = RelIncl X iff ( field b₂ = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in b₂ iff Y c= Z ) ) ) );