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 A1: ( not e2 in G .labeledE() & e2 in (G .labelEdge e1,val) .labeledE() ) ; :: thesis: ( e1 = e2 & e1 in the_Edges_of G )
then e1 in the_Edges_of G by Def21;
then the_ELabel_of (G .labelEdge e1,val) = (the_ELabel_of G) +* (e1 .--> val) by Th39;
then ( e2 in dom (the_ELabel_of G) or e2 in dom (e1 .--> val) ) by A1, FUNCT_4:13;
then e2 in {e1} by A1, FUNCOP_1:19;
hence e1 = e2 by TARSKI:def 1; :: thesis: e1 in the_Edges_of G
thus e1 in the_Edges_of G by A1, Def21; :: thesis: verum