let G be VGraph; :: thesis: for v, x being set holds G == G .labelVertex (v,x)
let e, x be set ; :: thesis: G == G .labelVertex (e,x)

now :: thesis: G == G .labelVertex (e,x)

per cases ( e in the_Vertices_of G or not e in the_Vertices_of G ) ;

suppose A1: e in the_Vertices_of G ; :: thesis: G == G .labelVertex (e,x)

A2: not VLabelSelector in _GraphSelectors by ENUMSET1:def 2;
A3: G .labelVertex (e,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (e .--> x))) by A1, Def22;
then A4: ( the_Source_of G = the_Source_of (G .labelVertex (e,x)) & the_Target_of G = the_Target_of (G .labelVertex (e,x)) ) by A2, GLIB_000:10;
( the_Vertices_of G = the_Vertices_of (G .labelVertex (e,x)) & the_Edges_of G = the_Edges_of (G .labelVertex (e,x)) ) by A3, A2, GLIB_000:10;
hence G == G .labelVertex (e,x) by A4; :: thesis: verum

end;

suppose not e in the_Vertices_of G ; :: thesis: G == G .labelVertex (e,x)

hence G == G .labelVertex (e,x) by Def22; :: thesis: verum

end;

end;

end;

hence G == G .labelVertex (e,x) ; :: thesis: verum