let G1 be _Graph; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( v1 = v2 implies ( v2 .inNeighbors() = (v1 .inNeighbors()) \ {v1} & v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} & v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} ) )
assume A1: v1 = v2 ; :: thesis: ( v2 .inNeighbors() = (v1 .inNeighbors()) \ {v1} & v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} & v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} )

now :: thesis: 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 ; :: thesis: ( ( x in v2 .inNeighbors() implies x in (v1 .inNeighbors()) \ {v1} ) & ( x in (v1 .inNeighbors()) \ {v1} implies x in v2 .inNeighbors() ) )

hereby :: thesis: ( x in (v1 .inNeighbors()) \ {v1} implies x in v2 .inNeighbors() )

assume A2: x in v2 .inNeighbors() ; :: thesis: x in (v1 .inNeighbors()) \ {v1}
then A3: x in v1 .inNeighbors() by A1, GLIB_000:82, TARSKI:def 3;
consider e being object such that
A4: e DJoins x,v2,G2 by A2, GLIB_000:69;
x <> v2 by A4, GLIB_000:136;
then not x in {v1} by A1, TARSKI:def 1;
hence x in (v1 .inNeighbors()) \ {v1} by A3, XBOOLE_0:def 5; :: thesis: verum

end;

assume x in (v1 .inNeighbors()) \ {v1} ; :: thesis: 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; :: thesis: verum

end;

hence A11: v2 .inNeighbors() = (v1 .inNeighbors()) \ {v1} by TARSKI:2; :: thesis: ( v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} & v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} )

now :: thesis: 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 ; :: thesis: ( ( x in v2 .outNeighbors() implies x in (v1 .outNeighbors()) \ {v1} ) & ( x in (v1 .outNeighbors()) \ {v1} implies x in v2 .outNeighbors() ) )

hereby :: thesis: ( x in (v1 .outNeighbors()) \ {v1} implies x in v2 .outNeighbors() )

assume A12: x in v2 .outNeighbors() ; :: thesis: x in (v1 .outNeighbors()) \ {v1}
then A13: x in v1 .outNeighbors() by A1, GLIB_000:82, TARSKI:def 3;
consider e being object such that
A14: e DJoins v2,x,G2 by A12, GLIB_000:70;
x <> v2 by A14, GLIB_000:136;
then not x in {v1} by A1, TARSKI:def 1;
hence x in (v1 .outNeighbors()) \ {v1} by A13, XBOOLE_0:def 5; :: thesis: verum

end;

assume x in (v1 .outNeighbors()) \ {v1} ; :: thesis: 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; :: thesis: verum

end;

hence A21: v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} by TARSKI:2; :: thesis: v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1}
thus v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} by A11, A21, XBOOLE_1:42; :: thesis: verum