let G be _finite _Graph; :: thesis: for L being MCS:Labeling of G

for v, x being set st x in dom (L `2) & x in G .AdjacentSet {v} & not x in dom (L `1) holds

((MCS:LabelAdjacent (L,v)) `2) . x = ((L `2) . x) + 1

let L be MCS:Labeling of G; :: thesis: for v, x being set st x in dom (L `2) & x in G .AdjacentSet {v} & not x in dom (L `1) holds

((MCS:LabelAdjacent (L,v)) `2) . x = ((L `2) . x) + 1

let v, x be set ; :: thesis: ( x in dom (L `2) & x in G .AdjacentSet {v} & not x in dom (L `1) implies ((MCS:LabelAdjacent (L,v)) `2) . x = ((L `2) . x) + 1 )

assume that

A1: x in dom (L `2) and

A2: x in G .AdjacentSet {v} and

A3: not x in dom (L `1) ; :: thesis: ((MCS:LabelAdjacent (L,v)) `2) . x = ((L `2) . x) + 1

set V2G = L `2 ;

set VLG = L `1 ;

set GL = MCS:LabelAdjacent (L,v);

set V2 = (MCS:LabelAdjacent (L,v)) `2 ;

x in (G .AdjacentSet {v}) \ (dom (L `1)) by A2, A3, XBOOLE_0:def 5;

hence ((MCS:LabelAdjacent (L,v)) `2) . x = ((L `2) . x) + 1 by A1, Def3; :: thesis: verum

for v, x being set st x in dom (L `2) & x in G .AdjacentSet {v} & not x in dom (L `1) holds

((MCS:LabelAdjacent (L,v)) `2) . x = ((L `2) . x) + 1

let L be MCS:Labeling of G; :: thesis: for v, x being set st x in dom (L `2) & x in G .AdjacentSet {v} & not x in dom (L `1) holds

((MCS:LabelAdjacent (L,v)) `2) . x = ((L `2) . x) + 1

let v, x be set ; :: thesis: ( x in dom (L `2) & x in G .AdjacentSet {v} & not x in dom (L `1) implies ((MCS:LabelAdjacent (L,v)) `2) . x = ((L `2) . x) + 1 )

assume that

A1: x in dom (L `2) and

A2: x in G .AdjacentSet {v} and

A3: not x in dom (L `1) ; :: thesis: ((MCS:LabelAdjacent (L,v)) `2) . x = ((L `2) . x) + 1

set V2G = L `2 ;

set VLG = L `1 ;

set GL = MCS:LabelAdjacent (L,v);

set V2 = (MCS:LabelAdjacent (L,v)) `2 ;

x in (G .AdjacentSet {v}) \ (dom (L `1)) by A2, A3, XBOOLE_0:def 5;

hence ((MCS:LabelAdjacent (L,v)) `2) . x = ((L `2) . x) + 1 by A1, Def3; :: thesis: verum