let G1 be _Graph; :: thesis: for G2 being SimpleGraph of G1
for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( v1,w1 are_adjacent iff v2,w2 are_adjacent )
let G2 be SimpleGraph of G1; :: thesis: for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( v1,w1 are_adjacent iff v2,w2 are_adjacent )
let v1, w1 be Vertex of G1; :: thesis: for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( v1,w1 are_adjacent iff v2,w2 are_adjacent )
let v2, w2 be Vertex of G2; :: thesis: ( v1 = v2 & w1 = w2 & v1 <> w1 implies ( v1,w1 are_adjacent iff v2,w2 are_adjacent ) )
assume A1: ( v1 = v2 & w1 = w2 & v1 <> w1 ) ; :: thesis: ( v1,w1 are_adjacent iff v2,w2 are_adjacent )
consider G9 being removeParallelEdges of G1 such that
A2: G2 is removeLoops of G9 by GLIB_009:119;
reconsider v9 = v2, w9 = w2 as Vertex of G9 by A2, GLIB_000:def 33;
( v1,w1 are_adjacent iff v9,w9 are_adjacent ) by A1, Th76;
hence ( v1,w1 are_adjacent iff v2,w2 are_adjacent ) by A1, A2, Th75; :: thesis: verum