:: deftheorem Def1 defines Relation-like RELAT_1:def 1 :
for IT being set holds
( IT is Relation-like iff for x being object st x in IT holds
ex y, z being object st x = [y,z] );