let G1 be _Graph; for G2 being removeLoops of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() = (v1 .inNeighbors()) \ {v1} & v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} & v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} )
let G2 be removeLoops of G1; for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() = (v1 .inNeighbors()) \ {v1} & v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} & v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} )
let v1 be Vertex of G1; for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() = (v1 .inNeighbors()) \ {v1} & v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} & v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} )
let v2 be Vertex of G2; ( v1 = v2 implies ( v2 .inNeighbors() = (v1 .inNeighbors()) \ {v1} & v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} & v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} ) )
assume A1:
v1 = v2
; ( v2 .inNeighbors() = (v1 .inNeighbors()) \ {v1} & v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} & v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} )
now for x being object holds
( ( x in v2 .inNeighbors() implies x in (v1 .inNeighbors()) \ {v1} ) & ( x in (v1 .inNeighbors()) \ {v1} implies x in v2 .inNeighbors() ) )let x be
object ;
( ( x in v2 .inNeighbors() implies x in (v1 .inNeighbors()) \ {v1} ) & ( x in (v1 .inNeighbors()) \ {v1} implies x in v2 .inNeighbors() ) )assume
x in (v1 .inNeighbors()) \ {v1}
;
x in v2 .inNeighbors() then A5:
(
x in v1 .inNeighbors() & not
x in {v1} )
by XBOOLE_0:def 5;
then consider e being
object such that A6:
e DJoins x,
v1,
G1
by GLIB_000:69;
A7:
e Joins x,
v1,
G1
by A6, GLIB_000:16;
x <> v1
by A5, TARSKI:def 1;
then A8:
not
e in G1 .loops()
by A7, GLIB_009:46;
e in the_Edges_of G1
by A6, GLIB_000:def 14;
then
e in (the_Edges_of G1) \ (G1 .loops())
by A8, XBOOLE_0:def 5;
then A9:
e in the_Edges_of G2
by GLIB_000:53;
A10:
(
x is
set &
e is
set )
by TARSKI:1;
then
e DJoins x,
v1,
G2
by A6, A9, GLIB_000:73;
hence
x in v2 .inNeighbors()
by A1, A10, GLIB_000:69;
verum end;
hence A11:
v2 .inNeighbors() = (v1 .inNeighbors()) \ {v1}
by TARSKI:2; ( v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} & v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} )
now for x being object holds
( ( x in v2 .outNeighbors() implies x in (v1 .outNeighbors()) \ {v1} ) & ( x in (v1 .outNeighbors()) \ {v1} implies x in v2 .outNeighbors() ) )let x be
object ;
( ( x in v2 .outNeighbors() implies x in (v1 .outNeighbors()) \ {v1} ) & ( x in (v1 .outNeighbors()) \ {v1} implies x in v2 .outNeighbors() ) )assume
x in (v1 .outNeighbors()) \ {v1}
;
x in v2 .outNeighbors() then A15:
(
x in v1 .outNeighbors() & not
x in {v1} )
by XBOOLE_0:def 5;
then consider e being
object such that A16:
e DJoins v1,
x,
G1
by GLIB_000:70;
A17:
e Joins v1,
x,
G1
by A16, GLIB_000:16;
x <> v1
by A15, TARSKI:def 1;
then A18:
not
e in G1 .loops()
by A17, GLIB_009:46;
e in the_Edges_of G1
by A16, GLIB_000:def 14;
then
e in (the_Edges_of G1) \ (G1 .loops())
by A18, XBOOLE_0:def 5;
then A19:
e in the_Edges_of G2
by GLIB_000:53;
A20:
(
x is
set &
e is
set )
by TARSKI:1;
then
e DJoins v1,
x,
G2
by A16, A19, GLIB_000:73;
hence
x in v2 .outNeighbors()
by A1, A20, GLIB_000:70;
verum end;
hence A21:
v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1}
by TARSKI:2; v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1}
thus
v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1}
by A11, A21, XBOOLE_1:42; verum