let G be _Graph; :: thesis: for e, X being set holds
( ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) iff e in G .edgesBetween X )
let e, X be set ; :: thesis: ( ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) iff e in G .edgesBetween X )
hereby :: thesis: ( e in G .edgesBetween X implies ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) )
assume ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) ; :: thesis: e in G .edgesBetween X
then ( e in G .edgesInto X & e in G .edgesOutOf X ) by Def26, Def27;
hence e in G .edgesBetween X by XBOOLE_0:def 4; :: thesis: verum
end;
assume e in G .edgesBetween X ; :: thesis: ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X )
then ( e in G .edgesInto X & e in G .edgesOutOf X ) by XBOOLE_0:def 4;
hence ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) by Def26, Def27; :: thesis: verum