let G1 be addEdge of G,v,e,w; :: thesis: G1 is loopfull

per cases ( ( v is Vertex of G & w is Vertex of G & not e in the_Edges_of G ) or not v is Vertex of G or not w is Vertex of G or e in the_Edges_of G ) ;

suppose A1: ( v is Vertex of G & w is Vertex of G & not e in the_Edges_of G ) ; :: thesis: G1 is loopfull

reconsider e = e as set by TARSKI:1;
G is removeEdge of G1,e by A1, GLIB_006:108;
hence G1 is loopfull ; :: thesis: verum

end;

suppose ( not v is Vertex of G or not w is Vertex of G or e in the_Edges_of G ) ; :: thesis: G1 is loopfull

then G == G1 by GLIB_006:def 11;
hence G1 is loopfull by Th4; :: thesis: verum

end;

end;