let G1 be _Graph; :: thesis: for G2 being DSimpleGraph 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 DSimpleGraph 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

consider H being removeDParallelEdges of G1 such that

A1: G2 is removeLoops of H by Th120;

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

reconsider v3 = v2 as Vertex of H by A1, GLIB_000:def 33;

v3 is endvertex by A2, Th114;

hence v2 is endvertex by A1, Th68; :: 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 DSimpleGraph 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

consider H being removeDParallelEdges of G1 such that

A1: G2 is removeLoops of H by Th120;

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

reconsider v3 = v2 as Vertex of H by A1, GLIB_000:def 33;

v3 is endvertex by A2, Th114;

hence v2 is endvertex by A1, Th68; :: thesis: verum