let e be set ; :: thesis: for G being Graph
for v1, v2, v3, v4 being Element of G st e orientedly_joins v1,v2 & e orientedly_joins v3,v4 holds
( v1 = v3 & v2 = v4 )
let G be Graph; :: thesis: for v1, v2, v3, v4 being Element of G st e orientedly_joins v1,v2 & e orientedly_joins v3,v4 holds
( v1 = v3 & v2 = v4 )
let v1, v2, v3, v4 be Element of G; :: thesis: ( e orientedly_joins v1,v2 & e orientedly_joins v3,v4 implies ( v1 = v3 & v2 = v4 ) )
assume that
A1: e orientedly_joins v1,v2 and
A2: e orientedly_joins v3,v4 ; :: thesis: ( v1 = v3 & v2 = v4 )
A3: the Source of G . e = v1 by A1, Def1;
the Target of G . e = v2 by A1, Def1;
hence ( v1 = v3 & v2 = v4 ) by A2, A3, Def1; :: thesis: verum