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