let G be _Graph; :: thesis: for e, X being set holds
( ( e in the_Edges_of G & ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) ) iff e in G .edgesInOut X )
let e, X be set ; :: thesis: ( ( e in the_Edges_of G & ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) ) iff e in G .edgesInOut X )

hereby :: thesis: ( e in G .edgesInOut X implies ( e in the_Edges_of G & ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) ) )

assume that
A1: e in the_Edges_of G and
A2: ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) ; :: thesis: e in G .edgesInOut X

now :: thesis: e in G .edgesInOut X

per cases ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) by A2;

suppose (the_Source_of G) . e in X ; :: thesis: e in G .edgesInOut X

then e in G .edgesOutOf X by A1, Def27;
hence e in G .edgesInOut X by XBOOLE_0:def 3; :: thesis: verum

end;

suppose (the_Target_of G) . e in X ; :: thesis: e in G .edgesInOut X

then e in G .edgesInto X by A1, Def26;
hence e in G .edgesInOut X by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence e in G .edgesInOut X ; :: thesis: verum

end;

assume e in G .edgesInOut X ; :: thesis: ( e in the_Edges_of G & ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) )
then ( e in G .edgesInto X or e in G .edgesOutOf X ) by XBOOLE_0:def 3;
hence ( e in the_Edges_of G & ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) ) by Def26, Def27; :: thesis: verum