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

proof

take e ; :: thesis: ( w .edgesInOut() = {e} & not e Joins w,w,G1 )
for e1 being object holds
( e1 in w .edgesInOut() iff e1 = e )

proof

let e1 be object ; :: thesis: ( e1 in w .edgesInOut() iff e1 = e )

hereby :: thesis: ( e1 = e implies e1 in w .edgesInOut() )

assume e1 in w .edgesInOut() ; :: thesis: e1 = e
then A3: ( e1 in the_Edges_of G1 & ( (the_Source_of G1) . e1 = w or (the_Target_of G1) . e1 = w ) ) by GLIB_000:61;
thus e1 = e :: thesis: verum

proof

assume A4: e1 <> e ; :: thesis: contradiction

per cases ( (the_Source_of G1) . e1 = w or (the_Target_of G1) . e1 = w ) by A3;

suppose (the_Source_of G1) . e1 = w ; :: thesis: contradiction

then e1 Joins (the_Target_of G1) . e1,w,G1 by A3, GLIB_000:def 13;
hence contradiction by A1, A2, A4, Th137; :: thesis: verum

end;

suppose (the_Target_of G1) . e1 = w ; :: thesis: contradiction

then e1 Joins (the_Source_of G1) . e1,w,G1 by A3, GLIB_000:def 13;
hence contradiction by A1, A2, A4, Th137; :: thesis: verum

end;

end;

end;

end;

assume A5: e1 = e ; :: thesis: e1 in w .edgesInOut()
e DJoins v1,v2,G1 by A1, Th135;
then ( e in the_Edges_of G1 & (the_Target_of G1) . e = w ) by A2, GLIB_000:def 14;
hence e1 in w .edgesInOut() by A5, GLIB_000:61; :: thesis: verum

end;

hence w .edgesInOut() = {e} by TARSKI:def 1; :: thesis: not e Joins w,w,G1
w <> v1 by A1, A2;
hence not e Joins w,w,G1 by A1, A2, Th137; :: thesis: verum

end;

hence w is endvertex by GLIB_000:def 51; :: thesis: verum