let G1 be _Graph; :: thesis: for G2 being removeParallelEdges 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 removeParallelEdges 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 A2: ( v2 is endvertex or v2 is isolated ) by GLIB_000:84;

not v1 is isolated by A1;

hence v2 is endvertex by A1, A2, Th111; :: 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 removeParallelEdges 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 A2: ( v2 is endvertex or v2 is isolated ) by GLIB_000:84;

not v1 is isolated by A1;

hence v2 is endvertex by A1, A2, Th111; :: thesis: verum