set G0 = the _trivial edgeless _Graph;
set v = the Vertex of the _trivial edgeless _Graph;
set w = the_Vertices_of the _trivial edgeless _Graph;
set e = the_Edges_of the _trivial edgeless _Graph;
set G1 = the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph;
A1: ( not the_Edges_of the _trivial edgeless _Graph in the_Edges_of the _trivial edgeless _Graph & not the_Vertices_of the _trivial edgeless _Graph in the_Vertices_of the _trivial edgeless _Graph ) ;
reconsider v1 = the Vertex of the _trivial edgeless _Graph, w1 = the_Vertices_of the _trivial edgeless _Graph as Vertex of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph by A1, GLIB_006:68, GLIB_006:129;
set f = the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph;
set G2 = the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1;
take the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 ; :: thesis: ( not the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 is non-multi & the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 is non-Dmulti )
A3: the_Edges_of the _trivial edgeless _Graph DJoins the Vertex of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 by A1, GLIB_006:70, GLIB_006:131;
A4: not the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph in the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph ;
then A5: the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph DJoins w1,v1, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 by GLIB_006:105;
ex e1, e2, v1, v2 being object st
( e1 Joins v1,v2, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 & e2 Joins v1,v2, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 & e1 <> e2 )

proof

take the_Edges_of the _trivial edgeless _Graph ; :: thesis: ex e2, v1, v2 being object st
( the_Edges_of the _trivial edgeless _Graph Joins v1,v2, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 & e2 Joins v1,v2, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 & the_Edges_of the _trivial edgeless _Graph <> e2 )
take the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph ; :: thesis: ex v1, v2 being object st
( the_Edges_of the _trivial edgeless _Graph Joins v1,v2, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 & the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph Joins v1,v2, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 & the_Edges_of the _trivial edgeless _Graph <> the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph )
take the Vertex of the _trivial edgeless _Graph ; :: thesis: ex v2 being object st
( the_Edges_of the _trivial edgeless _Graph Joins the Vertex of the _trivial edgeless _Graph,v2, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 & the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph Joins the Vertex of the _trivial edgeless _Graph,v2, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 & the_Edges_of the _trivial edgeless _Graph <> the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph )
take the_Vertices_of the _trivial edgeless _Graph ; :: thesis: ( the_Edges_of the _trivial edgeless _Graph Joins the Vertex of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 & the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph Joins the Vertex of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 & the_Edges_of the _trivial edgeless _Graph <> the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph )
thus the_Edges_of the _trivial edgeless _Graph Joins the Vertex of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 by A3, GLIB_000:16; :: thesis: ( the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph Joins the Vertex of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 & the_Edges_of the _trivial edgeless _Graph <> the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph )
thus the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph Joins the Vertex of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 by A5, GLIB_000:16; :: thesis: the_Edges_of the _trivial edgeless _Graph <> the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph
thus the_Edges_of the _trivial edgeless _Graph <> the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph ; :: thesis: verum

end;

hence not the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 is non-multi by GLIB_000:def 20; :: thesis: the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 is non-Dmulti
for e1, e2, v1, v2 being object st e1 DJoins v1,v2, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 & e2 DJoins v1,v2, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 holds
e1 = e2

proof

let e1, e2, v1, v2 be object ; :: thesis: ( e1 DJoins v1,v2, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 & e2 DJoins v1,v2, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 implies e1 = e2 )
assume A6: ( e1 DJoins v1,v2, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 & e2 DJoins v1,v2, the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 ) ; :: thesis: e1 = e2
then A7: ( e1 in the_Edges_of the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 & e2 in the_Edges_of the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 ) by GLIB_000:def 14;
the_Edges_of the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 = (the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph) \/ {(the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph)} by A4, GLIB_006:def 11
.= ((the_Edges_of the _trivial edgeless _Graph) \/ {(the_Edges_of the _trivial edgeless _Graph)}) \/ {(the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph)} by A1, GLIB_006:def 12
.= {(the_Edges_of the _trivial edgeless _Graph),(the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph)} by ENUMSET1:1 ;

per cases then ( ( e1 = the_Edges_of the _trivial edgeless _Graph & e2 = the_Edges_of the _trivial edgeless _Graph ) or ( e1 = the_Edges_of the _trivial edgeless _Graph & e2 = the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph ) or ( e1 = the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph & e2 = the_Edges_of the _trivial edgeless _Graph ) or ( e1 = the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph & e2 = the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph ) ) by A7, TARSKI:def 2;

suppose ( e1 = the_Edges_of the _trivial edgeless _Graph & e2 = the_Edges_of the _trivial edgeless _Graph ) ; :: thesis: e1 = e2

hence e1 = e2 ; :: thesis: verum

end;

suppose ( e1 = the_Edges_of the _trivial edgeless _Graph & e2 = the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph ) ; :: thesis: e1 = e2

then ( v1 = the Vertex of the _trivial edgeless _Graph & v2 = the_Vertices_of the _trivial edgeless _Graph & v1 = the_Vertices_of the _trivial edgeless _Graph & v2 = the Vertex of the _trivial edgeless _Graph ) by A3, A5, A6, GLIB_000:125;
then ( the Vertex of the _trivial edgeless _Graph = the_Vertices_of the _trivial edgeless _Graph & the Vertex of the _trivial edgeless _Graph in the_Vertices_of the _trivial edgeless _Graph ) ;
hence e1 = e2 ; :: thesis: verum

end;

suppose ( e1 = the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph & e2 = the_Edges_of the _trivial edgeless _Graph ) ; :: thesis: e1 = e2

then ( v1 = the Vertex of the _trivial edgeless _Graph & v2 = the_Vertices_of the _trivial edgeless _Graph & v1 = the_Vertices_of the _trivial edgeless _Graph & v2 = the Vertex of the _trivial edgeless _Graph ) by A3, A5, A6, GLIB_000:125;
then ( the Vertex of the _trivial edgeless _Graph = the_Vertices_of the _trivial edgeless _Graph & the Vertex of the _trivial edgeless _Graph in the_Vertices_of the _trivial edgeless _Graph ) ;
hence e1 = e2 ; :: thesis: verum

end;

suppose ( e1 = the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph & e2 = the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph ) ; :: thesis: e1 = e2

hence e1 = e2 ; :: thesis: verum

end;

end;

end;

hence the addEdge of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,w1, the_Edges_of the addAdjVertex of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the_Vertices_of the _trivial edgeless _Graph,v1 is non-Dmulti by GLIB_000:def 21; :: thesis: verum