:: deftheorem Def1 defines universal_friend FRIENDS1:def 1 :
for R being Relation
for x being Element of field R holds
( x is universal_friend iff for y being object st y in (field R) \ {x} holds
[x,y] in R );