let G be _Graph; :: thesis: ( ex f being VColoring of G st f is proper implies G is loopless )
given f being VColoring of G such that A1: f is proper ; :: thesis: G is loopless

now :: thesis: for v, e being object holds not e Joins v,v,G

given v, e being object such that A2: e Joins v,v,G ; :: thesis: contradiction
f . v = f . v ;
hence contradiction by A1, A2, Th10; :: thesis: verum

end;

hence G is loopless by GLIB_000:18; :: thesis: verum