:: deftheorem defines MCS:LabelAdjacent LEXBFS:def 21 :
for G being _finite _Graph
for L being MCS:Labeling of G
for v being set holds MCS:LabelAdjacent (L,v) = [(L `1),((L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1))];