let G be _Graph; :: thesis: ( G is 1 -edge implies G is non-multi )
assume G is 1 -edge ; :: thesis: G is non-multi
then G .size() = 1 by GLIB_013:def 4;
then consider e being object such that
A1: the_Edges_of G = {e} by CARD_2:42;
now :: thesis: for e1, e2, v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds
e1 = e2
let e1, e2, v1, v2 be object ; :: thesis: ( e1 Joins v1,v2,G & e2 Joins v1,v2,G implies e1 = e2 )
assume ( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ; :: thesis: e1 = e2
then ( e1 in the_Edges_of G & e2 in the_Edges_of G ) by GLIB_000:def 13;
then ( e1 = e & e2 = e ) by A1, TARSKI:def 1;
hence e1 = e2 ; :: thesis: verum
end;
hence G is non-multi by GLIB_000:def 20; :: thesis: verum