:: deftheorem Def1 defines Relation3 COLLSP:def 1 :
for X, b₂ being set holds
( b₂ is Relation3 of X iff b₂ c= [:X,X,X:] );