let G1, G2 be plain _Graph; :: thesis: ( G1 == G2 implies G1 = G2 )
dom G1 = _GraphSelectors by Def1;
then A1: dom G1 = dom G2 by Def1;
assume A2: G1 == G2 ; :: thesis: G1 = G2
for x being object st x in dom G1 holds
G1 . x = G2 . x

proof

let x be object ; :: thesis: ( x in dom G1 implies G1 . x = G2 . x )
assume x in dom G1 ; :: thesis: G1 . x = G2 . x
then x in _GraphSelectors by Def1;

per cases then ( x = VertexSelector or x = EdgeSelector or x = SourceSelector or x = TargetSelector ) by ENUMSET1:def 2, GLIB_000:def 5;

suppose A3: x = VertexSelector ; :: thesis: G1 . x = G2 . x

hence G1 . x = the_Vertices_of G1 by GLIB_000:def 6
.= the_Vertices_of G2 by A2, GLIB_000:def 34
.= G2 . x by A3, GLIB_000:def 6 ;
:: thesis: verum

end;

suppose A4: x = EdgeSelector ; :: thesis: G1 . x = G2 . x

hence G1 . x = the_Edges_of G1 by GLIB_000:def 7
.= the_Edges_of G2 by A2, GLIB_000:def 34
.= G2 . x by A4, GLIB_000:def 7 ;
:: thesis: verum

end;

suppose A5: x = SourceSelector ; :: thesis: G1 . x = G2 . x

thus G1 . x = the_Source_of G1 by A5, GLIB_000:def 8
.= the_Source_of G2 by A2, GLIB_000:def 34
.= G2 . x by A5, GLIB_000:def 8 ; :: thesis: verum

end;

suppose A6: x = TargetSelector ; :: thesis: G1 . x = G2 . x

hence G1 . x = the_Target_of G1 by GLIB_000:def 9
.= the_Target_of G2 by A2, GLIB_000:def 34
.= G2 . x by A6, GLIB_000:def 9 ;
:: thesis: verum

end;

end;

end;

hence G1 = G2 by A1, FUNCT_1:2; :: thesis: verum