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

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:13;
( 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:13;
hence G == G .labelVertex e,x by A4, GLIB_000:def 36; :: 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