let G1 be _Graph; :: thesis: for E being set

for G2 being reverseEdgeDirections of G1,E holds G1 .loops() = G2 .loops()

let E be set ; :: thesis: for G2 being reverseEdgeDirections of G1,E holds G1 .loops() = G2 .loops()

let G2 be reverseEdgeDirections of G1,E; :: thesis: G1 .loops() = G2 .loops()

for G2 being reverseEdgeDirections of G1,E holds G1 .loops() = G2 .loops()

let E be set ; :: thesis: for G2 being reverseEdgeDirections of G1,E holds G1 .loops() = G2 .loops()

let G2 be reverseEdgeDirections of G1,E; :: thesis: G1 .loops() = G2 .loops()

now :: thesis: for e being object holds

( ( e in G1 .loops() implies e in G2 .loops() ) & ( e in G2 .loops() implies e in G1 .loops() ) )

hence
G1 .loops() = G2 .loops()
by TARSKI:2; :: thesis: verum( ( e in G1 .loops() implies e in G2 .loops() ) & ( e in G2 .loops() implies e in G1 .loops() ) )

let e be object ; :: thesis: ( ( e in G1 .loops() implies e in G2 .loops() ) & ( e in G2 .loops() implies e in G1 .loops() ) )

then consider v being object such that

A2: e Joins v,v,G2 by Def2;

e Joins v,v,G1 by A2, GLIB_007:9;

hence e in G1 .loops() by Def2; :: thesis: verum

end;hereby :: thesis: ( e in G2 .loops() implies e in G1 .loops() )

assume
e in G2 .loops()
; :: thesis: e in G1 .loops() assume
e in G1 .loops()
; :: thesis: e in G2 .loops()

then consider v being object such that

A1: e Joins v,v,G1 by Def2;

e Joins v,v,G2 by A1, GLIB_007:9;

hence e in G2 .loops() by Def2; :: thesis: verum

end;then consider v being object such that

A1: e Joins v,v,G1 by Def2;

e Joins v,v,G2 by A1, GLIB_007:9;

hence e in G2 .loops() by Def2; :: thesis: verum

then consider v being object such that

A2: e Joins v,v,G2 by Def2;

e Joins v,v,G1 by A2, GLIB_007:9;

hence e in G1 .loops() by Def2; :: thesis: verum