set VL = (the_VLabel_of G) +* (v .--> x);
set G2 = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x)));

hereby :: thesis:

A1: dom ((the_VLabel_of G) +* (v .--> x)) = (dom (the_VLabel_of G)) \/ (dom (v .--> x)) by FUNCT_4:def 1;
assume A2: v in the_Vertices_of G ; :: thesis:

now :: thesis:

let y be object ; :: thesis:
assume A3: y in dom ((the_VLabel_of G) +* (v .--> x)) ; :: thesis:

now :: thesis:

per cases by A1, A3, XBOOLE_0:def 3;

suppose A4: y in dom (the_VLabel_of G) ; :: thesis:

dom (the_VLabel_of G) c= the_Vertices_of G by Lm2;
hence y in the_Vertices_of G by A4; :: thesis:

end;

suppose y in dom (v .--> x) ; :: thesis:

then y in {v} ;
hence y in the_Vertices_of G by A2, TARSKI:def 1; :: thesis:

end;

end;

end;

hence y in the_Vertices_of G ; :: thesis:

end;

then dom ((the_VLabel_of G) +* (v .--> x)) c= the_Vertices_of G by TARSKI:def 3;
then reconsider V1 = (the_VLabel_of G) +* (v .--> x) as PartFunc of (the_Vertices_of G),(rng ((the_VLabel_of G) +* (v .--> x))) by RELSET_1:4;
G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) = G .set (VLabelSelector,V1) ;
hence G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) is VGraph ; :: thesis:

end;

thus ( not v in the_Vertices_of G implies G is VGraph ) ; :: thesis: