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

hereby :: thesis: ( v2,w2 are_adjacent implies v1,w1 are_adjacent )

assume v1,w1 are_adjacent ; :: thesis: v2,w2 are_adjacent
then w1 in (v1 .allNeighbors()) \ {v1} by A1, Th42, ZFMISC_1:56;
then w2 in v2 .allNeighbors() by A1, GLIBPRE0:63;
hence v2,w2 are_adjacent by Th42; :: thesis: verum

end;

assume v2,w2 are_adjacent ; :: thesis: v1,w1 are_adjacent
then w2 in v2 .allNeighbors() by Th42;
then w1 in (v1 .allNeighbors()) \ {v1} by A1, GLIBPRE0:63;
hence v1,w1 are_adjacent by Th42, ZFMISC_1:56; :: thesis: verum