set k = (G .order()) -' n;
set L1 = (L `1) +* (v .--> ((G .order()) -' n));
A1: dom ((L `1) +* (v .--> ((G .order()) -' n))) = (dom (L `1)) \/ {v} by Lm1;
rng ((L `1) +* (v .--> ((G .order()) -' n))) c= NAT ;
then (L `1) +* (v .--> ((G .order()) -' n)) in PFuncs ((the_Vertices_of G),NAT) by A1, PARTFUN1:def 3;
then reconsider M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] as MCS:Labeling of G by ZFMISC_1:87;
MCS:LabelAdjacent (M,v) is MCS:Labeling of G ;
hence ex b<sub>1</sub>, M being MCS:Labeling of G st
( M = [((L `1) +* (v .--> ((G .order()) -' n))),(L `2)] & b₁ = MCS:LabelAdjacent (M,v) ) ; :: thesis: verum