Description: An undirected hypergraph with two (different) vertices is complete iff there is an edge between these two vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Proof shortened by Alexander van der Vekens, 16-Dec-2017) (Revised by AV, 3-Nov-2020)