let e be set ; :: thesis: for G being Graph
for v1, v2 being Element of G st e orientedly_joins v1,v2 holds
e joins v1,v2
let G be Graph; :: thesis: for v1, v2 being Element of G st e orientedly_joins v1,v2 holds
e joins v1,v2
let v1, v2 be Element of G; :: thesis: ( e orientedly_joins v1,v2 implies e joins v1,v2 )
assume A1: e orientedly_joins v1,v2 ; :: thesis: e joins v1,v2
then A2: the Source of G . e = v1 by Def1;
the Target of G . e = v2 by A1, Def1;
hence e joins v1,v2 by A2, GRAPH_1:def 10; :: thesis: verum