let G1 be loopless _Graph; :: thesis: for G2 being DSimpleGraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is isolated iff v2 is isolated )

let G2 be DSimpleGraph of G1; :: thesis: for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is isolated iff v2 is isolated )

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 holds

( v1 is isolated iff v2 is isolated )

let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies ( v1 is isolated iff v2 is isolated ) )

assume A2: v1 = v2 ; :: thesis: ( v1 is isolated iff v2 is isolated )

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

G2 == H by A1, Th58;

then ( v3 is isolated iff v2 is isolated ) by GLIB_000:97;

hence ( v1 is isolated iff v2 is isolated ) by A2, Th112; :: thesis: verum

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is isolated iff v2 is isolated )

let G2 be DSimpleGraph of G1; :: thesis: for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is isolated iff v2 is isolated )

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 holds

( v1 is isolated iff v2 is isolated )

let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies ( v1 is isolated iff v2 is isolated ) )

assume A2: v1 = v2 ; :: thesis: ( v1 is isolated iff v2 is isolated )

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

G2 == H by A1, Th58;

then ( v3 is isolated iff v2 is isolated ) by GLIB_000:97;

hence ( v1 is isolated iff v2 is isolated ) by A2, Th112; :: thesis: verum