let G2 be _Graph; :: thesis: for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
( e DJoins v1,v2,G1 & e Joins v1,v2,G1 )
let v1, e be object ; :: thesis: for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
( e DJoins v1,v2,G1 & e Joins v1,v2,G1 )
let v2 be Vertex of G2; :: thesis: for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
( e DJoins v1,v2,G1 & e Joins v1,v2,G1 )
let G1 be addAdjVertex of G2,v1,e,v2; :: thesis: ( not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 implies ( e DJoins v1,v2,G1 & e Joins v1,v2,G1 ) )
assume A1: ( not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis: ( e DJoins v1,v2,G1 & e Joins v1,v2,G1 )
e in {e} by TARSKI:def 1;
then e in (the_Edges_of G2) \/ {e} by XBOOLE_0:def 3;
then A3: e in the_Edges_of G1 by A1, Def14;
( ((the_Source_of G2) +* (e .--> v1)) . e = v1 & ((the_Target_of G2) +* (e .--> v2)) . e = v2 ) by FUNCT_4:113;
then ( (the_Source_of G1) . e = v1 & (the_Target_of G1) . e = v2 ) by A1, Def14;
hence e DJoins v1,v2,G1 by A3, GLIB_000:def 14; :: thesis: e Joins v1,v2,G1
hence e Joins v1,v2,G1 by GLIB_000:16; :: thesis: verum