let G be _Graph; :: thesis: for e, v, w being object st e Joins v,w,G & v <> w holds
not e in G .loops()
let e, v, w be object ; :: thesis: ( e Joins v,w,G & v <> w implies not e in G .loops() )
assume A1: ( e Joins v,w,G & v <> w ) ; :: thesis: not e in G .loops()
assume e in G .loops() ; :: thesis: contradiction
then consider u being object such that
A2: e Joins u,u,G by Def2;
( u = v & u = w ) by A1, A2, GLIB_000:15;
hence contradiction by A1; :: thesis: verum