theorem :: FRIENDS1:14

for FSG being Friendship_Graph st not FSG is empty holds
FSG is with_universal_friend