theorem :: LEXBFS:63

for G being _finite _Graph
for L being MCS:Labeling of G
for v being set st dom (L `2) = the_Vertices_of G holds
dom ((MCS:LabelAdjacent (L,v)) `2) = the_Vertices_of G by Def3;