let G1 be addAdjVertex of G,v1,e,v2; :: thesis: G1 is loopless

per cases ( ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G ) or ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) or ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) ) ) ;

suppose A1: ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis: G1 is loopless

consider G3 being addVertex of G,v2 such that
A2: G1 is addEdge of G3,v1,e,v2 by A1, Th129;
reconsider w1 = v1 as Vertex of G3 by A1, Th72;
reconsider w2 = v2 as Vertex of G3 by Th98;
A3: w1 <> w2 by A1;
thus G1 is loopless by A2, A3, Th116; :: thesis: verum

end;

suppose A4: ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis: G1 is loopless

consider G3 being addVertex of G,v1 such that
A5: G1 is addEdge of G3,v1,e,v2 by A4, Th130;
reconsider w2 = v2 as Vertex of G3 by A4, Th72;
reconsider w1 = v1 as Vertex of G3 by Th98;
A6: w1 <> w2 by A4;
thus G1 is loopless by A5, A6, Th116; :: thesis: verum

end;

suppose ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) ) ; :: thesis: G1 is loopless

then G1 == G by Def12;
hence G1 is loopless by GLIB_000:89; :: thesis: verum

end;

end;