let G1 be _Graph; :: thesis: for E being Subset of (the_Edges_of G1)
for G2 being reverseEdgeDirections of G1,E holds
( G1 tolerates G2 iff E c= G1 .loops() )
let E be Subset of (the_Edges_of G1); :: thesis: for G2 being reverseEdgeDirections of G1,E holds
( G1 tolerates G2 iff E c= G1 .loops() )
let G2 be reverseEdgeDirections of G1,E; :: thesis: ( G1 tolerates G2 iff E c= G1 .loops() )

hereby :: thesis: ( E c= G1 .loops() implies G1 tolerates G2 )

assume A1: G1 tolerates G2 ; :: thesis: E c= G1 .loops()
assume not E c= G1 .loops() ; :: thesis: contradiction
then E \ (G1 .loops()) <> {} by XBOOLE_1:37;
then consider e being object such that
A2: e in E \ (G1 .loops()) by XBOOLE_0:def 1;
set v = (the_Source_of G1) . e;
set w = (the_Target_of G1) . e;
A3: e in E by A2, XBOOLE_0:def 5;
then A4: e DJoins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by GLIB_000:def 14;
then e DJoins (the_Target_of G1) . e,(the_Source_of G1) . e,G2 by A3, GLIB_007:7;
then (the_Source_of G1) . e = (the_Target_of G1) . e by A1, A4, Th17;
then e in G1 .loops() by A4, GLIB_009:45;
hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum

end;

assume A5: E c= G1 .loops() ; :: thesis: G1 tolerates G2

now :: thesis: for e, v1, w1, v2, w2 being object st e DJoins v1,w1,G1 & e DJoins v2,w2,G2 holds
( v1 = v2 & w1 = w2 )

let e, v1, w1, v2, w2 be object ; :: thesis: ( e DJoins v1,w1,G1 & e DJoins v2,w2,G2 implies ( b₂ = b₄ & b₃ = b₅ ) )
assume A6: ( e DJoins v1,w1,G1 & e DJoins v2,w2,G2 ) ; :: thesis: ( b₂ = b₄ & b₃ = b₅ )

per cases ( e in E or not e in E ) ;

suppose A7: e in E ; :: thesis: ( b₂ = b₄ & b₃ = b₅ )

then consider u being object such that
A8: e DJoins u,u,G1 by A5, GLIB_009:45;
A9: ( v1 = u & w1 = u ) by A6, A8, GLIB_000:125;
e DJoins w1,v1,G2 by A6, A7, GLIB_007:7;
hence ( v1 = v2 & w1 = w2 ) by A6, A9, GLIB_000:125; :: thesis: verum

end;

suppose not e in E ; :: thesis: ( b₂ = b₄ & b₃ = b₅ )

then e DJoins v1,w1,G2 by A6, GLIB_007:8;
hence ( v1 = v2 & w1 = w2 ) by A6, GLIB_000:125; :: thesis: verum

end;

end;

end;

hence G1 tolerates G2 by Th17; :: thesis: verum