:: deftheorem Def21 defines .labelEdge GLIB_003:def 21 :
for G being EGraph
for e, x being object holds
( ( e in the_Edges_of G implies G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) ) & ( not e in the_Edges_of G implies G .labelEdge (e,x) = G ) );