let G2 be _Graph; :: thesis: for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
for e1, w1, w2 being object st e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 & not ( w1 = v1 & w2 = v2 ) holds
( w1 = v2 & w2 = v1 )
let v1, v2 be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
for e1, w1, w2 being object st e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 & not ( w1 = v1 & w2 = v2 ) holds
( w1 = v2 & w2 = v1 )
let e be object ; :: thesis: for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
for e1, w1, w2 being object st e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 & not ( w1 = v1 & w2 = v2 ) holds
( w1 = v2 & w2 = v1 )
let G1 be addEdge of G2,v1,e,v2; :: thesis: ( not e in the_Edges_of G2 implies for e1, w1, w2 being object st e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 & not ( w1 = v1 & w2 = v2 ) holds
( w1 = v2 & w2 = v1 ) )
assume A1: not e in the_Edges_of G2 ; :: thesis: for e1, w1, w2 being object st e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 & not ( w1 = v1 & w2 = v2 ) holds
( w1 = v2 & w2 = v1 )
let e1, w1, w2 be object ; :: thesis: ( e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 & not ( w1 = v1 & w2 = v2 ) implies ( w1 = v2 & w2 = v1 ) )
assume A2: ( e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 ) ; :: thesis: ( ( w1 = v1 & w2 = v2 ) or ( w1 = v2 & w2 = v1 ) )
then A3: e = e1 by A1, Th110;
e DJoins v1,v2,G1 by A1, Th109;
then e1 Joins v1,v2,G1 by A3, GLIB_000:16;
hence ( ( w1 = v1 & w2 = v2 ) or ( w1 = v2 & w2 = v1 ) ) by A2, GLIB_000:15; :: thesis: verum