let G1 be _Graph; :: thesis: for E being set
for G2 being reverseEdgeDirections of G1,E holds
( G1 is loopfull iff G2 is loopfull )
let E be set ; :: thesis: for G2 being reverseEdgeDirections of G1,E holds
( G1 is loopfull iff G2 is loopfull )
let G2 be reverseEdgeDirections of G1,E; :: thesis: ( G1 is loopfull iff G2 is loopfull )

hereby :: thesis: ( G2 is loopfull implies G1 is loopfull )

assume A1: G1 is loopfull ; :: thesis: G2 is loopfull

now :: thesis: for v being Vertex of G2 ex e being object st e Joins v,v,G2

let v be Vertex of G2; :: thesis: ex e being object st e Joins v,v,G2
v is Vertex of G1 by GLIB_007:4;
then consider e being object such that
A2: e Joins v,v,G1 by A1;
take e = e; :: thesis: e Joins v,v,G2
thus e Joins v,v,G2 by A2, GLIB_007:9; :: thesis: verum

end;

hence G2 is loopfull ; :: thesis: verum

end;

assume A3: G2 is loopfull ; :: thesis: G1 is loopfull

now :: thesis: for v being Vertex of G1 ex e being object st e Joins v,v,G1

let v be Vertex of G1; :: thesis: ex e being object st e Joins v,v,G1
v is Vertex of G2 by GLIB_007:4;
then consider e being object such that
A4: e Joins v,v,G2 by A3;
take e = e; :: thesis: e Joins v,v,G1
thus e Joins v,v,G1 by A4, GLIB_007:9; :: thesis: verum

end;

hence G1 is loopfull ; :: thesis: verum