:: deftheorem Def21 defines MCS:Update LEXBFS:def 22 :
for G being _finite _Graph
for L being MCS:Labeling of G
for v being Vertex of G
for n being Nat
for b₅ being MCS:Labeling of G holds
( b₅ = MCS:Update (L,v,n) iff ex M being MCS:Labeling of G st
( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & b₅ = MCS:LabelAdjacent (M,v) ) );