theorem Th61: :: LEXBFS:61

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