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))) by GLIB_000:def 36;

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

assume A2: e in the_Edges_of G ; :: thesis: G .set ELabelSelector ,((the_ELabel_of G) +* (e .--> x)) is EGraph
A3: ELabelSelector in dom G by Def5;
A4: dom G c= dom (G .set ELabelSelector ,((the_ELabel_of G) +* (e .--> x))) by FUNCT_4:11;
A5: 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} by FUNCOP_1:19 ;

now

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

now

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

suppose A7: 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 A7; :: thesis: verum

end;

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

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

end;

end;

end;

hence z in the_Edges_of G ; :: thesis: verum

end;

then A8: 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;
(G .set ELabelSelector ,((the_ELabel_of G) +* (e .--> x))) . ELabelSelector = (the_ELabel_of G) +* (e .--> x) by GLIB_000:11;
hence G .set ELabelSelector ,((the_ELabel_of G) +* (e .--> x)) is EGraph by A3, A4, A8, Def5; :: thesis: verum

end;

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