let G be EGraph; :: thesis: for e, x being set holds G == G .labelEdge e,x
let e, x be set ; :: thesis: G == G .labelEdge e,x

now

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

suppose A1: e in the_Edges_of G ; :: thesis: G == G .labelEdge e,x

A2: not ELabelSelector in _GraphSelectors by ENUMSET1:def 2;
A3: G .labelEdge e,x = G .set ELabelSelector ,((the_ELabel_of G) +* (e .--> x)) by A1, Def21;
then A4: ( the_Source_of G = the_Source_of (G .labelEdge e,x) & the_Target_of G = the_Target_of (G .labelEdge e,x) ) by A2, GLIB_000:13;
( the_Vertices_of G = the_Vertices_of (G .labelEdge e,x) & the_Edges_of G = the_Edges_of (G .labelEdge e,x) ) by A3, A2, GLIB_000:13;
hence G == G .labelEdge e,x by A4, GLIB_000:def 36; :: thesis: verum

end;

suppose not e in the_Edges_of G ; :: thesis: G == G .labelEdge e,x

hence G == G .labelEdge e,x by Def21; :: thesis: verum

end;

end;

end;

hence G == G .labelEdge e,x ; :: thesis: verum