:: deftheorem Def6 defines XEdge GRAPHSP:def 6 :
for G being oriented Graph
for v1, v2 being Vertex of G st ex e being set st
( e in the carrier' of G & e orientedly_joins v1,v2 ) holds
for b₄ being set holds
( b₄ = XEdge (v1,v2) iff ex e being set st
( b₄ = e & e in the carrier' of G & e orientedly_joins v1,v2 ) );