let G be Graph; :: thesis: for v1, v2 being Element of G
for e being set st e joins v1,v2 holds
e joins v2,v1
let v1, v2 be Element of G; :: thesis: for e being set st e joins v1,v2 holds
e joins v2,v1
let e be set ; :: thesis: ( e joins v1,v2 implies e joins v2,v1 )
assume e joins v1,v2 ; :: thesis: e joins v2,v1
then ( ( 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 GRAPH_1:def 10;
hence e joins v2,v1 by GRAPH_1:def 10; :: thesis: verum