set EL = (the_ELabel_of G) +* (e .--> x);
set G2 = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x)));
G == G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Lm3;
then A1: the_Edges_of G = the_Edges_of (G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x)))) ;

hereby :: thesis: ( not e in the_Edges_of G implies G is EGraph )

A2: dom ((the_ELabel_of G) +* (e .--> x)) = (dom (the_ELabel_of G)) \/ (dom (e .--> x)) by FUNCT_4:def 1
.= (dom (the_ELabel_of G)) \/ {e} ;
assume A3: e in the_Edges_of G ; :: thesis: G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) is EGraph

now :: thesis: for z being object st z in dom ((the_ELabel_of G) +* (e .--> x)) holds
z in the_Edges_of G

let z be object ; :: thesis: ( z in dom ((the_ELabel_of G) +* (e .--> x)) implies z in the_Edges_of G )
assume A4: z in dom ((the_ELabel_of G) +* (e .--> x)) ; :: thesis: z in the_Edges_of G

now :: thesis: z in the_Edges_of G

per cases ( z in dom (the_ELabel_of G) or z in {e} ) by A2, A4, XBOOLE_0:def 3;

suppose A5: z in dom (the_ELabel_of G) ; :: thesis: z in the_Edges_of G

dom (the_ELabel_of G) c= the_Edges_of G by Lm1;
hence z in the_Edges_of G by A5; :: thesis: verum

end;

suppose z in {e} ; :: thesis: z in the_Edges_of G

hence z in the_Edges_of G by A3, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence z in the_Edges_of G ; :: thesis: verum

end;

then A6: dom ((the_ELabel_of G) +* (e .--> x)) c= the_Edges_of (G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x)))) by A1, TARSKI:def 3;
A7: (G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x)))) . ELabelSelector = (the_ELabel_of G) +* (e .--> x) by GLIB_000:8;
( ELabelSelector in dom G & dom G c= dom (G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x)))) ) by Def5, FUNCT_4:10;
hence G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) is EGraph by A6, A7, Def5; :: thesis: verum

end;

thus ( not e in the_Edges_of G implies G is EGraph ) ; :: thesis: verum