let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies for u1 being Vertex of G1
for u2 being Vertex of G2 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 G1
for u2 being Vertex of G2 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 G1; :: thesis: for u2 being Vertex of G2 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 G2; :: 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, Th50;
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,(G1 .AdjacentSet {u1}) by Def5;
A5: H2 is inducedSubgraph of G2,(G2 .AdjacentSet {u2}) by Def5;

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

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

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

end;

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

then the_Vertices_of H1 = G1 .AdjacentSet {u1} by A4, GLIB_000:def 37;
then A9: the_Vertices_of H1 = the_Vertices_of H2 by A5, A3, GLIB_000:def 37;
G1 is Subgraph of G2 by A1, GLIB_000:87;
then A10: G1 .edgesBetween (G1 .AdjacentSet {u1}) c= G2 .edgesBetween (G1 .AdjacentSet {u1}) by GLIB_000:76;
A11: the_Edges_of H1 = G1 .edgesBetween (G1 .AdjacentSet {u1}) by A4, A8, GLIB_000:def 37;
G2 is Subgraph of G1 by A1, GLIB_000:87;
then A12: G2 .edgesBetween (G1 .AdjacentSet {u1}) c= G1 .edgesBetween (G1 .AdjacentSet {u1}) by GLIB_000:76;
G2 is Subgraph of G1 by A1, GLIB_000:87;
then A13: H2 is Subgraph of G1 by GLIB_000:43;
the_Edges_of H2 = G2 .edgesBetween (G2 .AdjacentSet {u2}) by A5, A3, A8, GLIB_000:def 37;
then the_Edges_of H1 = the_Edges_of H2 by A3, A11, A10, A12;
hence H1 == H2 by A9, A13, GLIB_000:86; :: thesis: verum

end;

end;