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 ;
A4: (MCS:LabelAdjacent L,v) `2 = (L `2 ) .incSubset ((G .AdjacentSet {v}) \ (dom (L `1 ))),1 by MCART_1:def 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, A4, Def4; :: thesis: verum