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 & v1 is endvertex holds
v2 is endvertex
let G2 be removeLoops of G1; for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds
v2 is endvertex
let v1 be Vertex of G1; for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds
v2 is endvertex
let v2 be Vertex of G2; ( v1 = v2 & v1 is endvertex implies v2 is endvertex )
assume A1:
( v1 = v2 & v1 is endvertex )
; v2 is endvertex
then consider e being object such that
A2:
( v1 .edgesInOut() = {e} & not e Joins v1,v1,G1 )
by GLIB_000:def 51;
reconsider e = e as set by TARSKI:1;
e in {e}
by TARSKI:def 1;
then consider w1 being Vertex of G1 such that
A3:
e Joins v1,w1,G1
by A2, GLIB_000:64;
A4:
not e in G1 .loops()
by A2, A3, Th46;
A5:
( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ (G1 .loops()) )
by GLIB_000:53;
then reconsider w2 = w1 as Vertex of G2 ;
e in the_Edges_of G1
by A3, GLIB_000:def 13;
then
e in the_Edges_of G2
by A4, A5, XBOOLE_0:def 5;
then
e Joins v2,w2,G2
by A1, A3, GLIB_000:73;
then
e in v2 .edgesInOut()
by GLIB_000:64;
hence
v2 is endvertex
by A1, GLIB_000:def 49, GLIB_000:84; verum