The
friendship theorem of states that the finite graphs with the property that every two vertices have exactly one neighbor in common are exactly the friendship graphs. Informally, if a group of people has the property that every pair of people has exactly one friend in common, then there must be one person who is a friend to all the others. However, for infinite graphs, there can be many different graphs with the same
cardinality that have this property. A
combinatorial proof of the friendship theorem was given by Mertzios and Unger. Another proof was given by
Craig Huneke. A formalised proof in
Metamath was reported by Alexander van der Vekens in October 2018 on the Metamath mailing list. ==Labeling and colouring==