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