let G be _Graph; :: thesis: for e being set
for v1, v2 being Vertex of G holds
( not e Joins v1,v2,G or ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) )
let e be set ; :: thesis: for v1, v2 being Vertex of G holds
( not e Joins v1,v2,G or ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) )
let v1, v2 be Vertex of G; :: thesis: ( not e Joins v1,v2,G or ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) )
assume A1: e Joins v1,v2,G ; :: thesis: ( ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) )
then A2: e in the_Edges_of G by Def15;

now

per cases ( ( (the_Source_of G) . e = v1 & (the_Target_of G) . e = v2 ) or ( (the_Source_of G) . e = v2 & (the_Target_of G) . e = v1 ) ) by A1, Def15;

suppose ( (the_Source_of G) . e = v1 & (the_Target_of G) . e = v2 ) ; :: thesis: ( ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) )

hence ( ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ) by A2, Lm8, Lm9; :: thesis: verum

end;

suppose ( (the_Source_of G) . e = v2 & (the_Target_of G) . e = v1 ) ; :: thesis: ( ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) )

hence ( ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ) by A2, Lm8, Lm9; :: thesis: verum

end;

end;

end;

hence ( ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) ) ; :: thesis: verum