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;

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) )
;

end;

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;then A7: H1 == G2 by A1;

H2 == G2 by A5, A3, A6, GLIB_000:def 37;

hence H1 == H2 by A7; :: thesis: verum

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;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