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 GL = MCS:LabelAdjacent L,v;
set V2 = (MCS:LabelAdjacent L,v) `2 ;
set VLG = L `1 ;
set V2G = L `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