let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies for u1 being Vertex of
for u2 being Vertex of st u1 = u2 holds
for H1 being AdjGraph of G1,{u1}
for H2 being AdjGraph of G2,{u2} holds H1 == H2 )
assume A1: G1 == G2 ; :: thesis: for u1 being Vertex of
for u2 being Vertex of st u1 = u2 holds
for H1 being AdjGraph of G1,{u1}
for H2 being AdjGraph of G2,{u2} holds H1 == H2
let u1 be Vertex of ; :: thesis: for u2 being Vertex of st u1 = u2 holds
for H1 being AdjGraph of G1,{u1}
for H2 being AdjGraph of G2,{u2} holds H1 == H2
let u2 be Vertex of ; :: thesis: ( u1 = u2 implies for H1 being AdjGraph of G1,{u1}
for H2 being AdjGraph of G2,{u2} holds H1 == H2 )
assume A2: u1 = u2 ; :: thesis: for H1 being AdjGraph of G1,{u1}
for H2 being AdjGraph of G2,{u2} holds H1 == H2
set G2Adj = G2 .AdjacentSet {u2};
set G1Adj = G1 .AdjacentSet {u1};
A3: G1 .AdjacentSet {u1} = G2 .AdjacentSet {u2} by A1, A2, Th51;
let H1 be AdjGraph of G1,{u1}; :: thesis: for H2 being AdjGraph of G2,{u2} holds H1 == H2
let H2 be AdjGraph of G2,{u2}; :: thesis: H1 == H2
A4: H1 is inducedSubgraph of G1,{u1} by Def5;
A5: H2 is inducedSubgraph of G2,{u2} by Def5;

per cases ( not G1 .AdjacentSet {u1} is non empty Subset of or G1 .AdjacentSet {u1} is non empty Subset of ) ;

suppose A6: G1 .AdjacentSet {u1} is not non empty Subset of ; :: thesis: H1 == H2

then H1 == G1 by A4, GLIB_000:def 39;
then A7: H1 == G2 by A1, GLIB_000:88;
H2 == G2 by A5, A3, A6, GLIB_000:def 39;
hence H1 == H2 by A7, GLIB_000:88; :: thesis: verum

end;

suppose A8: G1 .AdjacentSet {u1} is non empty Subset of ; :: thesis: H1 == H2

then the_Vertices_of H1 = G1 .AdjacentSet {u1} by A4, GLIB_000:def 39;
then A9: the_Vertices_of H1 = the_Vertices_of H2 by A5, A3, GLIB_000:def 39;
G1 is Subgraph of G2 by A1, GLIB_000:90;
then A10: G1 .edgesBetween (G1 .AdjacentSet {u1}) c= G2 .edgesBetween (G1 .AdjacentSet {u1}) by GLIB_000:79;
A11: the_Edges_of H1 = G1 .edgesBetween (G1 .AdjacentSet {u1}) by A4, A8, GLIB_000:def 39;
G2 is Subgraph of G1 by A1, GLIB_000:90;
then A12: G2 .edgesBetween (G1 .AdjacentSet {u1}) c= G1 .edgesBetween (G1 .AdjacentSet {u1}) by GLIB_000:79;
G2 is Subgraph of G1 by A1, GLIB_000:90;
then A13: H2 is Subgraph of G1 by GLIB_000:46;
the_Edges_of H2 = G2 .edgesBetween (G2 .AdjacentSet {u2}) by A5, A3, A8, GLIB_000:def 39;
then the_Edges_of H1 = the_Edges_of H2 by A3, A11, A10, A12, XBOOLE_0:def 10;
hence H1 == H2 by A9, A13, GLIB_000:89; :: thesis: verum

end;

end;