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 & v1 is endvertex holds

v2 is endvertex

let G2 be removeLoops of G1; :: thesis: 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; :: thesis: for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds

v2 is endvertex

let v2 be Vertex of G2; :: thesis: ( v1 = v2 & v1 is endvertex implies v2 is endvertex )

assume A1: ( v1 = v2 & v1 is endvertex ) ; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: thesis: for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds

v2 is endvertex

let v2 be Vertex of G2; :: thesis: ( v1 = v2 & v1 is endvertex implies v2 is endvertex )

assume A1: ( v1 = v2 & v1 is endvertex ) ; :: thesis: 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; :: thesis: verum