:: deftheorem Def8 defines id RELAT_1:def 10 :
for X being set
for b₂ being Relation holds
( b₂ = id X iff for x, y being object holds
( [x,y] in b₂ iff ( x in X & x = y ) ) );