theorem :: FRIENDS1:13
for FSG being Friendship_Graph
for x, y being Element of field FSG st x is universal_friend & x <> y holds
ex z being object st
( Im (FSG,y) = {x,z} & Im (FSG,z) = {x,y} )