:: deftheorem Def3 defines friendship_graph_like FRIENDS1:def 3 :
for R being Relation holds
( R is friendship_graph_like iff for x, y being object st x in field R & y in field R & x <> y holds
ex z being object st (Im (R,x)) /\ (Coim (R,y)) = {z} );