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()

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() ) )

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

hereby :: thesis: ( e in G2 .loops() implies 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;

assume e in G2 .loops() ; :: thesis: 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;

hence G1 .loops() = G2 .loops() by TARSKI:2; :: thesis: verum