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 :: thesis: G == G .labelEdge (e,x)

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:10;
( 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:10;
hence G == G .labelEdge (e,x) by A4; :: 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