let G be _Graph; :: thesis: for e being set
for v being Vertex of G holds
( e in v .edgesInOut() iff ( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ) )
let e be set ; :: thesis: for v being Vertex of G holds
( e in v .edgesInOut() iff ( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ) )
let v be Vertex of G; :: thesis: ( e in v .edgesInOut() iff ( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ) )
hereby :: thesis: ( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) implies e in v .edgesInOut() )
assume A1: e in v .edgesInOut() ; :: thesis: ( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) )
hence e in the_Edges_of G ; :: thesis: ( (the_Source_of G) . e = v or (the_Target_of G) . e = v )
( e in v .edgesIn() or e in v .edgesOut() ) by A1, XBOOLE_0:def 3;
hence ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) by Lm7, Lm8; :: thesis: verum
end;
assume ( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ) ; :: thesis: e in v .edgesInOut()
then ( e in v .edgesIn() or e in v .edgesOut() ) by Lm7, Lm8;
hence e in v .edgesInOut() by XBOOLE_0:def 3; :: thesis: verum