let G2 be _Graph; 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; 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 ; 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; ( 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
; 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 ; ( 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 )
; ( ( 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; verum