let G be _Graph; :: thesis:
let e, X be set ; :: thesis:

hereby :: thesis:

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:

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

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

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

end;

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

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

end;

end;

end;

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

end;

assume e in G .edgesInOut X ; :: thesis:
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: