theorem Th12: :: FRIENDS1:12

for x being object
for FSG being Friendship_Graph st FSG is without_universal_friend & x in field FSG holds
card (field FSG) = 1 + ((card (Im (FSG,x))) * ((card (Im (FSG,x))) - 1))