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