theorem Th28: :: GLIB_000:28

for G being _Graph
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 )