let G1 be _Graph; for G2 being removeParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
v2 .allNeighbors() = v1 .allNeighbors()
let G2 be removeParallelEdges of G1; for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
v2 .allNeighbors() = v1 .allNeighbors()
let v1 be Vertex of G1; for v2 being Vertex of G2 st v1 = v2 holds
v2 .allNeighbors() = v1 .allNeighbors()
let v2 be Vertex of G2; ( v1 = v2 implies v2 .allNeighbors() = v1 .allNeighbors() )
assume A1:
v1 = v2
; v2 .allNeighbors() = v1 .allNeighbors()
consider E being RepEdgeSelection of G1 such that
A2:
G2 is inducedSubgraph of G1, the_Vertices_of G1,E
by GLIB_009:def 7;
the_Edges_of G1 = G1 .edgesBetween (the_Vertices_of G1)
by GLIB_000:34;
then
( E c= G1 .edgesBetween (the_Vertices_of G1) & the_Vertices_of G1 c= the_Vertices_of G1 )
;
then A3:
the_Edges_of G2 = E
by A2, GLIB_000:def 37;
A4:
v2 .allNeighbors() c= v1 .allNeighbors()
by A1, GLIB_000:82;
now for x being object st x in v1 .allNeighbors() holds
x in v2 .allNeighbors() let x be
object ;
( x in v1 .allNeighbors() implies x in v2 .allNeighbors() )assume
x in v1 .allNeighbors()
;
x in v2 .allNeighbors() then consider e0 being
object such that A5:
e0 Joins v1,
x,
G1
by GLIB_000:71;
consider e being
object such that A6:
(
e Joins v1,
x,
G1 &
e in E )
and
for
e9 being
object st
e9 Joins v1,
x,
G1 &
e9 in E holds
e9 = e
by A5, GLIB_009:def 5;
A7:
(
x is
set &
e is
set )
by TARSKI:1;
then
e Joins v1,
x,
G2
by A3, A6, GLIB_000:73;
hence
x in v2 .allNeighbors()
by A1, A7, GLIB_000:71;
verum end;
then
v1 .allNeighbors() c= v2 .allNeighbors()
by TARSKI:def 3;
hence
v2 .allNeighbors() = v1 .allNeighbors()
by A4, XBOOLE_0:def 10; verum