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