let G be EGraph; for e, x being set holds G == G .labelEdge (e,x)
let e, x be set ; G == G .labelEdge (e,x)
now 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
;
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;
verum end;
hence
G == G .labelEdge (e,x)
; verum