let G be EGraph; :: thesis: for e1, e2, x being set st not e2 in G .labeledE() & e2 in (G .labelEdge (e1,x)) .labeledE() holds
( e1 = e2 & e1 in the_Edges_of G )
let e1, e2, val be set ; :: thesis: ( not e2 in G .labeledE() & e2 in (G .labelEdge (e1,val)) .labeledE() implies ( e1 = e2 & e1 in the_Edges_of G ) )
set Gn = G .labelEdge (e1,val);
assume that
A1: not e2 in G .labeledE() and
A2: e2 in (G .labelEdge (e1,val)) .labeledE() ; :: thesis: ( e1 = e2 & e1 in the_Edges_of G )
e1 in the_Edges_of G by A1, A2, Def21;
then the_ELabel_of (G .labelEdge (e1,val)) = (the_ELabel_of G) +* (e1 .--> val) by Th32;
then ( e2 in dom (the_ELabel_of G) or e2 in dom (e1 .--> val) ) by A2, FUNCT_4:12;
then e2 in {e1} by A1;
hence e1 = e2 by TARSKI:def 1; :: thesis: e1 in the_Edges_of G
thus e1 in the_Edges_of G by A1, A2, Def21; :: thesis: verum