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

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