let G be _Graph; :: thesis:
assume A1: for v being Vertex of G holds
( v .inNeighbors() c= (the_Vertices_of G) \ {v} or v .outNeighbors() c= (the_Vertices_of G) \ {v} or v .allNeighbors() c= (the_Vertices_of G) \ {v} ) ; :: thesis:

now :: thesis:

let v be object ; :: thesis:
given e being object such that A2: e Joins v,v,G ; :: thesis:
reconsider w = v as Vertex of G by A2, GLIB_000:13;
e DJoins v,v,G by A2, GLIB_000:16;
then A3: ( v in w .inNeighbors() & v in w .outNeighbors() & v in w .allNeighbors() ) by A2, GLIB_000:69, GLIB_000:70, GLIB_000:71;
v in (the_Vertices_of G) \ {w}

proof

per cases by A1;

suppose w .inNeighbors() c= (the_Vertices_of G) \ {w} ; :: thesis:

hence v in (the_Vertices_of G) \ {w} by A3; :: thesis:

end;

suppose w .outNeighbors() c= (the_Vertices_of G) \ {w} ; :: thesis:

hence v in (the_Vertices_of G) \ {w} by A3; :: thesis:

end;

suppose w .allNeighbors() c= (the_Vertices_of G) \ {w} ; :: thesis:

hence v in (the_Vertices_of G) \ {w} by A3; :: thesis:

end;

end;

end;

hence contradiction by ZFMISC_1:56; :: thesis:

end;

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