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

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

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: G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) is VGraph

now :: thesis: for y being object st y in dom ((the_VLabel_of G) +* (v .--> x)) holds
y in the_Vertices_of G

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

now :: thesis: y in the_Vertices_of G

per cases ( y in dom (the_VLabel_of G) or y in dom (v .--> x) ) by A1, A3, XBOOLE_0:def 3;

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

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

end;

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

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

end;

end;

end;

hence y in the_Vertices_of G ; :: thesis: verum

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: verum

end;

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