let G2 be _Graph; for v being object
for V being set
for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( ( for e being object holds
( not e Joins v,v,G1 & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2 ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) ) ) )
let v be object ; for V being set
for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( ( for e being object holds
( not e Joins v,v,G1 & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2 ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) ) ) )
let V be set ; for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( ( for e being object holds
( not e Joins v,v,G1 & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2 ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) ) ) )
let G1 be addAdjVertexToAll of G2,v,V; ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 implies ( ( for e being object holds
( not e Joins v,v,G1 & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2 ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) ) ) ) )
assume A1:
( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 )
; ( ( for e being object holds
( not e Joins v,v,G1 & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2 ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) ) ) )
hereby ex E being set st
( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) ) )
let e be
object ;
( not e Joins v,v,G1 & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2 ) ) ) )
not
e DJoins v,
v,
G1
by A1, Th38;
hence
not
e Joins v,
v,
G1
by GLIB_000:16;
for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2 ) )let v1 be
object ;
( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2 ) )thus
( not
v1 in V implies not
e Joins v1,
v,
G1 )
for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2proof
assume A2:
not
v1 in V
;
not e Joins v1,v,G1
assume
e Joins v1,
v,
G1
;
contradiction
then
(
e DJoins v1,
v,
G1 or
e DJoins v,
v1,
G1 )
by GLIB_000:16;
hence
contradiction
by A1, A2, Th38;
verum
end; let v2 be
object ;
( v1 <> v & v2 <> v & e DJoins v1,v2,G1 implies e DJoins v1,v2,G2 )assume A3:
(
v1 <> v &
v2 <> v &
e DJoins v1,
v2,
G1 )
;
e DJoins v1,v2,G2thus
e DJoins v1,
v2,
G2
by A1, A3, Th40;
verum
end;
set E = V --> (the_Edges_of G2);
take
V --> (the_Edges_of G2)
; ( card V = card (V --> (the_Edges_of G2)) & V --> (the_Edges_of G2) misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ (V --> (the_Edges_of G2)) & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in V --> (the_Edges_of G2) & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) ) )
thus
card V = card (V --> (the_Edges_of G2))
by Lm8; ( V --> (the_Edges_of G2) misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ (V --> (the_Edges_of G2)) & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in V --> (the_Edges_of G2) & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) ) )
(the_Edges_of G2) /\ (V --> (the_Edges_of G2)) = {}
by Lm6;
hence
V --> (the_Edges_of G2) misses the_Edges_of G2
by XBOOLE_0:def 7; ( the_Edges_of G1 = (the_Edges_of G2) \/ (V --> (the_Edges_of G2)) & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in V --> (the_Edges_of G2) & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) ) )
thus
the_Edges_of G1 = (the_Edges_of G2) \/ (V --> (the_Edges_of G2))
by A1, Def2; for v1 being object st v1 in V holds
ex e1 being object st
( e1 in V --> (the_Edges_of G2) & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) )
let v1 be object ; ( v1 in V implies ex e1 being object st
( e1 in V --> (the_Edges_of G2) & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) )
assume A4:
v1 in V
; ex e1 being object st
( e1 in V --> (the_Edges_of G2) & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) )
set e1 = [v1,(the_Edges_of G2)];
take
[v1,(the_Edges_of G2)]
; ( [v1,(the_Edges_of G2)] in V --> (the_Edges_of G2) & [v1,(the_Edges_of G2)] Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
[v1,(the_Edges_of G2)] = e2 ) )
the_Edges_of G2 in {(the_Edges_of G2)}
by TARSKI:def 1;
then
[v1,(the_Edges_of G2)] in [:V,{(the_Edges_of G2)}:]
by A4, ZFMISC_1:def 2;
hence
[v1,(the_Edges_of G2)] in V --> (the_Edges_of G2)
by FUNCOP_1:def 2; ( [v1,(the_Edges_of G2)] Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
[v1,(the_Edges_of G2)] = e2 ) )
A5:
[v1,(the_Edges_of G2)] DJoins v,v1,G1
by A1, A4, Th42;
hence
[v1,(the_Edges_of G2)] Joins v1,v,G1
by GLIB_000:16; for e2 being object st e2 Joins v1,v,G1 holds
[v1,(the_Edges_of G2)] = e2
let e2 be object ; ( e2 Joins v1,v,G1 implies [v1,(the_Edges_of G2)] = e2 )
assume A6:
e2 Joins v1,v,G1
; [v1,(the_Edges_of G2)] = e2
not e2 DJoins v1,v,G1
by A1, Th38;
then
e2 DJoins v,v1,G1
by A6, GLIB_000:16;
hence
[v1,(the_Edges_of G2)] = e2
by A1, A5, Th38; verum