theorem Th62: :: LEXBFS:62

for G being _finite _Graph
for L being MCS:Labeling of G
for v, x being set st x in dom (L `2) & x in G .AdjacentSet {v} & not x in dom (L `1) holds
((MCS:LabelAdjacent (L,v)) `2) . x = ((L `2) . x) + 1