let G be finite _Graph; :: thesis: for L being MCS:Labeling of G
for v, x being set st not x in G .AdjacentSet {v} holds
(L `2) . x = ((MCS:LabelAdjacent (L,v)) `2) . x
let L be MCS:Labeling of G; :: thesis: for v, x being set st not x in G .AdjacentSet {v} holds
(L `2) . x = ((MCS:LabelAdjacent (L,v)) `2) . x
let v, x be set ; :: thesis: ( not x in G .AdjacentSet {v} implies (L `2) . x = ((MCS:LabelAdjacent (L,v)) `2) . x )
assume A1: not x in G .AdjacentSet {v} ; :: thesis: (L `2) . x = ((MCS:LabelAdjacent (L,v)) `2) . x
set V2G = L `2 ;
set VLG = L `1 ;
set GL = MCS:LabelAdjacent (L,v);
set V2 = (MCS:LabelAdjacent (L,v)) `2 ;
A2: (MCS:LabelAdjacent (L,v)) `2 = (L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1) by MCART_1:def 2;
not x in (G .AdjacentSet {v}) \ (dom (L `1)) by A1, XBOOLE_0:def 5;
hence (L `2) . x = ((MCS:LabelAdjacent (L,v)) `2) . x by A2, Def4; :: thesis: verum