Metamath Proof Explorer


Theorem clnbgrssvtx

Description: The closed neighborhood of a vertex K in a graph is a subset of all vertices of the graph. (Contributed by AV, 9-May-2025)

Ref Expression
Hypothesis clnbgrvtxel.v V = Vtx G
Assertion clnbgrssvtx G ClNeighbVtx K V

Proof

Step Hyp Ref Expression
1 clnbgrvtxel.v V = Vtx G
2 1 clnbgrisvtx n G ClNeighbVtx K n V
3 2 ssriv G ClNeighbVtx K V