let G be _Graph; :: thesis: ( ( 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} ) ) implies G is loopless )
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: G is loopless

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

let v be object ; :: thesis: for e being object holds not e Joins v,v,G
given e being object such that A2: e Joins v,v,G ; :: thesis: contradiction
reconsider w = v as Vertex of G by A2, FUNCT_2:5;
e DJoins v,v,G by A2;
then A3: ( v in w .inNeighbors() & v in w .outNeighbors() & v in w .allNeighbors() ) by A2, Th69, Th70, Th71;
v in (the_Vertices_of G) \ {w}

proof

per cases ( w .inNeighbors() c= (the_Vertices_of G) \ {w} or w .outNeighbors() c= (the_Vertices_of G) \ {w} or w .allNeighbors() c= (the_Vertices_of G) \ {w} ) by A1;

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

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

end;

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

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

end;

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

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

end;

end;

end;

hence contradiction by ZFMISC_1:56; :: thesis: verum

end;

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