let G3 be _Graph; for v being object
for V1, V2 being set
for G1 being addAdjVertexAll of G3,v,V1 \/ V2
for G2 being removeEdges of G1,(G1 .edgesBetween (V2,{v})) st V1 \/ V2 c= the_Vertices_of G3 & not v in the_Vertices_of G3 & V1 misses V2 holds
G2 is addAdjVertexAll of G3,v,V1
let v be object ; for V1, V2 being set
for G1 being addAdjVertexAll of G3,v,V1 \/ V2
for G2 being removeEdges of G1,(G1 .edgesBetween (V2,{v})) st V1 \/ V2 c= the_Vertices_of G3 & not v in the_Vertices_of G3 & V1 misses V2 holds
G2 is addAdjVertexAll of G3,v,V1
let V1, V2 be set ; for G1 being addAdjVertexAll of G3,v,V1 \/ V2
for G2 being removeEdges of G1,(G1 .edgesBetween (V2,{v})) st V1 \/ V2 c= the_Vertices_of G3 & not v in the_Vertices_of G3 & V1 misses V2 holds
G2 is addAdjVertexAll of G3,v,V1
let G1 be addAdjVertexAll of G3,v,V1 \/ V2; for G2 being removeEdges of G1,(G1 .edgesBetween (V2,{v})) st V1 \/ V2 c= the_Vertices_of G3 & not v in the_Vertices_of G3 & V1 misses V2 holds
G2 is addAdjVertexAll of G3,v,V1
let G2 be removeEdges of G1,(G1 .edgesBetween (V2,{v})); ( V1 \/ V2 c= the_Vertices_of G3 & not v in the_Vertices_of G3 & V1 misses V2 implies G2 is addAdjVertexAll of G3,v,V1 )
assume that
A1:
( V1 \/ V2 c= the_Vertices_of G3 & not v in the_Vertices_of G3 )
and
A2:
V1 misses V2
; G2 is addAdjVertexAll of G3,v,V1
A3:
G1 is Supergraph of G2
by GLIB_006:57;
V1 c= V1 \/ V2
by XBOOLE_1:7;
then A4:
( V1 c= the_Vertices_of G3 & not v in the_Vertices_of G3 )
by A1, XBOOLE_1:1;
consider E being set such that
A5:
( card (V1 \/ V2) = card E & E misses the_Edges_of G3 )
and
A6:
the_Edges_of G1 = (the_Edges_of G3) \/ E
and
A7:
for v1 being object st v1 in V1 \/ V2 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 ) )
by A1, Def4;
reconsider F = E \ (G1 .edgesBetween (V2,{v})) as set ;
E = G1 .edgesBetween ((V1 \/ V2),{v})
by A1, A5, A6, Th58;
then
E = (G1 .edgesBetween (V1,{v})) \/ (G1 .edgesBetween (V2,{v}))
by GLIB_006:20;
then A9:
F = G1 .edgesBetween (V1,{v})
by XBOOLE_1:88, A2, GLIB_006:19;
for e being object st e in the_Edges_of G3 holds
e in (the_Edges_of G3) \ (G1 .edgesBetween (V2,{v}))
proof
let e be
object ;
( e in the_Edges_of G3 implies e in (the_Edges_of G3) \ (G1 .edgesBetween (V2,{v})) )
assume A10:
e in the_Edges_of G3
;
e in (the_Edges_of G3) \ (G1 .edgesBetween (V2,{v}))
not
e in G1 .edgesBetween (
V2,
{v})
proof
assume
e in G1 .edgesBetween (
V2,
{v})
;
contradiction
then
e SJoins V2,
{v},
G1
by GLIB_000:def 30;
then consider w being
object such that A11:
(
w in V2 &
e Joins w,
v,
G1 )
by GLIB_006:17;
w in V1 \/ V2
by A11, XBOOLE_1:7, TARSKI:def 3;
then consider e1 being
object such that A12:
(
e1 in E &
e1 Joins w,
v,
G1 )
and A13:
for
e2 being
object st
e2 Joins w,
v,
G1 holds
e1 = e2
by A7;
A14:
E /\ (the_Edges_of G3) = {}
by A5, XBOOLE_0:def 7;
e1 = e
by A11, A13;
hence
contradiction
by A10, A12, A14, Lm7;
verum
end;
hence
e in (the_Edges_of G3) \ (G1 .edgesBetween (V2,{v}))
by A10, XBOOLE_0:def 5;
verum
end;
then
the_Edges_of G3 c= (the_Edges_of G3) \ (G1 .edgesBetween (V2,{v}))
by TARSKI:def 3;
then A15:
(the_Edges_of G3) \ (G1 .edgesBetween (V2,{v})) = the_Edges_of G3
by XBOOLE_0:def 10;
A16: the_Edges_of G2 =
(the_Edges_of G1) \ (G1 .edgesBetween (V2,{v}))
by GLIB_000:53
.=
(the_Edges_of G3) \/ F
by A6, A15, XBOOLE_1:42
;
A17:
now ( the_Vertices_of G2 = (the_Vertices_of G3) \/ {v} & ( for e being object holds
( not e Joins v,v,G2 & ( for v1 being object holds
( ( not v1 in V1 implies not e Joins v1,v,G2 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G2 holds
e DJoins v1,v2,G3 ) ) ) ) ) & ex F being set st
( card V1 = card F & F misses the_Edges_of G3 & the_Edges_of G2 = (the_Edges_of G3) \/ F & ( for v1 being object st v1 in V1 holds
ex e1 being object st
( e1 in F & e1 Joins v1,v,G2 & ( for e2 being object st e2 Joins v1,v,G2 holds
e1 = e2 ) ) ) ) )
the_Vertices_of G1 = (the_Vertices_of G3) \/ {v}
by A1, Def4;
hence
the_Vertices_of G2 = (the_Vertices_of G3) \/ {v}
by GLIB_000:53;
( ( for e being object holds
( not e Joins v,v,G2 & ( for v1 being object holds
( ( not v1 in V1 implies not e Joins v1,v,G2 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G2 holds
e DJoins v1,v2,G3 ) ) ) ) ) & ex F being set st
( card V1 = card F & F misses the_Edges_of G3 & the_Edges_of G2 = (the_Edges_of G3) \/ F & ( for v1 being object st v1 in V1 holds
ex e1 being object st
( e1 in F & e1 Joins v1,v,G2 & ( for e2 being object st e2 Joins v1,v,G2 holds
e1 = e2 ) ) ) ) )hereby ex F being set st
( card V1 = card F & F misses the_Edges_of G3 & the_Edges_of G2 = (the_Edges_of G3) \/ F & ( for v1 being object st v1 in V1 holds
ex e1 being object st
( e1 in F & e1 Joins v1,v,G2 & ( for e2 being object st e2 Joins v1,v,G2 holds
e1 = e2 ) ) ) )
let e be
object ;
( not e Joins v,v,G2 & ( for v1 being object holds
( ( not v1 in V1 implies not e Joins v1,v,G2 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G2 holds
e DJoins v1,v2,G3 ) ) ) )A18:
v is
set
by TARSKI:1;
thus
not
e Joins v,
v,
G2
for v1 being object holds
( ( not v1 in V1 implies not e Joins v1,v,G2 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G2 holds
e DJoins v1,v2,G3 ) )let v1 be
object ;
( ( not v1 in V1 implies not e Joins v1,v,G2 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G2 holds
e DJoins v1,v2,G3 ) )A19:
v1 is
set
by TARSKI:1;
thus
( not
v1 in V1 implies not
e Joins v1,
v,
G2 )
for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G2 holds
e DJoins v1,v2,G3proof
assume A20:
not
v1 in V1
;
not e Joins v1,v,G2
assume A21:
e Joins v1,
v,
G2
;
contradiction
then A22:
e Joins v1,
v,
G1
by A3, A18, A19, GLIB_006:70;
then
v1 in V1 \/ V2
by A1, Def4;
then A23:
v1 in V2
by A20, XBOOLE_0:def 3;
v in {v}
by TARSKI:def 1;
then
e SJoins V2,
{v},
G1
by A22, A23, GLIB_000:17;
then A24:
e in G1 .edgesBetween (
V2,
{v})
by GLIB_000:def 30;
the_Edges_of G2 = (the_Edges_of G1) \ (G1 .edgesBetween (V2,{v}))
by GLIB_000:53;
then
not
e in the_Edges_of G2
by A24, XBOOLE_0:def 5;
hence
contradiction
by A21, GLIB_000:def 13;
verum
end; let v2 be
object ;
( v1 <> v & v2 <> v & e DJoins v1,v2,G2 implies e DJoins v1,v2,G3 )A25:
v2 is
set
by TARSKI:1;
assume A26:
(
v1 <> v &
v2 <> v )
;
( e DJoins v1,v2,G2 implies e DJoins v1,v2,G3 )assume
e DJoins v1,
v2,
G2
;
e DJoins v1,v2,G3then
e DJoins v1,
v2,
G1
by A3, A19, A25, GLIB_006:70;
hence
e DJoins v1,
v2,
G3
by A1, A26, Def4;
verum
end; take F =
F;
( card V1 = card F & F misses the_Edges_of G3 & the_Edges_of G2 = (the_Edges_of G3) \/ F & ( for v1 being object st v1 in V1 holds
ex e1 being object st
( e1 in F & e1 Joins v1,v,G2 & ( for e2 being object st e2 Joins v1,v,G2 holds
e1 = e2 ) ) ) )reconsider W =
V1 as
Subset of
(V1 \/ V2) by XBOOLE_1:7;
consider f being
Function of
W,
(G1 .edgesBetween (W,{v})) such that A27:
(
f is
one-to-one &
f is
onto )
and
for
w being
object st
w in W holds
f . w Joins w,
v,
G1
by A1, Th57;
A28:
dom f = W
rng f = G1 .edgesBetween (
W,
{v})
by A27, FUNCT_2:def 3;
hence
card V1 = card F
by A9, CARD_1:5, A27, A28, WELLORD2:def 4;
( F misses the_Edges_of G3 & the_Edges_of G2 = (the_Edges_of G3) \/ F & ( for v1 being object st v1 in V1 holds
ex e1 being object st
( e1 in F & e1 Joins v1,v,G2 & ( for e2 being object st e2 Joins v1,v,G2 holds
e1 = e2 ) ) ) )thus
F misses the_Edges_of G3
by A5, XBOOLE_1:63;
( the_Edges_of G2 = (the_Edges_of G3) \/ F & ( for v1 being object st v1 in V1 holds
ex e1 being object st
( e1 in F & e1 Joins v1,v,G2 & ( for e2 being object st e2 Joins v1,v,G2 holds
e1 = e2 ) ) ) )thus
the_Edges_of G2 = (the_Edges_of G3) \/ F
by A16;
for v1 being object st v1 in V1 holds
ex e1 being object st
( e1 in F & e1 Joins v1,v,G2 & ( for e2 being object st e2 Joins v1,v,G2 holds
e1 = e2 ) )let v1 be
object ;
( v1 in V1 implies ex e1 being object st
( e1 in F & e1 Joins v1,v,G2 & ( for e2 being object st e2 Joins v1,v,G2 holds
e1 = e2 ) ) )assume A30:
v1 in V1
;
ex e1 being object st
( e1 in F & e1 Joins v1,v,G2 & ( for e2 being object st e2 Joins v1,v,G2 holds
e1 = e2 ) )then
v1 in V1 \/ V2
by XBOOLE_0:def 3;
then consider e1 being
object such that A31:
(
e1 in E &
e1 Joins v1,
v,
G1 )
and A32:
for
e2 being
object st
e2 Joins v1,
v,
G1 holds
e1 = e2
by A7;
take e1 =
e1;
( e1 in F & e1 Joins v1,v,G2 & ( for e2 being object st e2 Joins v1,v,G2 holds
e1 = e2 ) )
v in {v}
by TARSKI:def 1;
then
e1 SJoins V1,
{v},
G1
by A30, A31, GLIB_000:17;
hence
e1 in F
by A9, GLIB_000:def 30;
( e1 Joins v1,v,G2 & ( for e2 being object st e2 Joins v1,v,G2 holds
e1 = e2 ) )then A33:
e1 in the_Edges_of G2
by A16, XBOOLE_0:def 3;
thus
e1 Joins v1,
v,
G2
for e2 being object st e2 Joins v1,v,G2 holds
e1 = e2let e2 be
object ;
( e2 Joins v1,v,G2 implies e1 = e2 )assume A35:
e2 Joins v1,
v,
G2
;
e1 = e2
(
v1 is
set &
v is
set )
by TARSKI:1;
hence
e1 = e2
by A32, A35, GLIB_000:72;
verum end;
G2 is Supergraph of G3
hence
G2 is addAdjVertexAll of G3,v,V1
by A4, A17, Def4; verum