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 Th71;
thus contradiction by A1, A2; :: 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, FUNCT_2:5;
not v0 in v0 .allNeighbors() by A3;
hence contradiction by A4, Th71; :: thesis: verum

end;

hence G is loopless by Th18; :: thesis: verum