let G2 be _Graph; for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2
for w being Vertex of G1 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & w = v1 holds
w is endvertex
let v1, e be object ; for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2
for w being Vertex of G1 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & w = v1 holds
w is endvertex
let v2 be Vertex of G2; for G1 being addAdjVertex of G2,v1,e,v2
for w being Vertex of G1 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & w = v1 holds
w is endvertex
let G1 be addAdjVertex of G2,v1,e,v2; for w being Vertex of G1 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & w = v1 holds
w is endvertex
let w be Vertex of G1; ( not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & w = v1 implies w is endvertex )
assume that
A1:
( not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 )
and
A2:
w = v1
; w is endvertex
ex e1 being object st
( w .edgesInOut() = {e1} & not e1 Joins w,w,G1 )
hence
w is endvertex
by GLIB_000:def 51; verum