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:
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 ;
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 ;
hence e in G1 .loops() by Def2; :: thesis: verum
end;
hence G1 .loops() = G2 .loops() by TARSKI:2; :: thesis: verum