let G be Graph; :: thesis: for v1, v2, v3, v4 being Element of the carrier 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 the carrier 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 ) ) & ( ( the Source of G . e = v3 & the Target of G . e = v4 ) or ( the Source of G . e = v4 & the Target of G . e = v3 ) ) ) by A1, A2, GRAPH_1:def 10;
hence ( ( v1 = v3 & v2 = v4 ) or ( v1 = v4 & v2 = v3 ) ) ; :: thesis: verum