let G be _Graph; :: thesis: ( G is loopless iff for v being Vertex of G holds not v in v .allNeighbors() )
hereby :: thesis: ( ( for v being Vertex of G holds not v in v .allNeighbors() ) implies G is loopless )
assume A1: G is loopless ; :: thesis: for v being Vertex of G holds not v in v .allNeighbors()
let v be Vertex of G; :: thesis: not v in v .allNeighbors()
thus not v in v .allNeighbors() :: thesis: verum
proof
assume v in v .allNeighbors() ; :: thesis: contradiction
then consider e being object such that
A2: e Joins v,v,G by GLIB_000:71;
thus contradiction by A1, A2, GLIB_000:18; :: thesis: verum
end;
end;
assume A3: for v being Vertex of G holds not v in v .allNeighbors() ; :: thesis: G is loopless
for v, e being object holds not e Joins v,v,G
proof
given v being object such that A4: ex e being object st e Joins v,v,G ; :: thesis: contradiction
reconsider v0 = v as Vertex of G by A4, GLIB_000:13;
not v0 in v0 .allNeighbors() by A3;
hence contradiction by A4, GLIB_000:71; :: thesis: verum
end;
hence G is loopless by GLIB_000:18; :: thesis: verum