let G3 be _Graph; :: thesis:
let v be object ; :: thesis:
let V1, V2 be set ; :: thesis:
let G1 be addAdjVertexAll of G3,v,V1 \/ V2; :: thesis:
let G2 be removeEdges of G1,(G1 .edgesBetween (V2,{v})); :: thesis:
assume that
A1: ( V1 \/ V2 c= the_Vertices_of G3 & not v in the_Vertices_of G3 ) and
A2: V1 misses V2 ; :: thesis:
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_000:105;
then A9: F = G1 .edgesBetween (V1,{v}) by XBOOLE_1:88, A2, GLIB_000:104;
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 ; :: thesis:
assume A10: e in the_Edges_of G3 ; :: thesis:
not e in G1 .edgesBetween (V2,{v})

proof

assume e in G1 .edgesBetween (V2,{v}) ; :: thesis:
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_000:102;
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; :: thesis:

end;

hence e in (the_Edges_of G3) \ (G1 .edgesBetween (V2,{v})) by A10, XBOOLE_0:def 5; :: thesis:

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 :: thesis:

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; :: thesis:

hereby :: thesis:

let e be object ; :: thesis:
A18: v is set by TARSKI:1;
thus not e Joins v,v,G2 :: thesis:

proof

assume e Joins v,v,G2 ; :: thesis:
then e Joins v,v,G1 by A3, A18, GLIB_006:70;
hence contradiction by A1, Def4; :: thesis:

end;

let v1 be object ; :: thesis:
A19: v1 is set by TARSKI:1;
thus ( not v1 in V1 implies not e Joins v1,v,G2 ) :: thesis:

proof

assume A20: not v1 in V1 ; :: thesis:
assume A21: e Joins v1,v,G2 ; :: thesis:
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; :: thesis:

end;

let v2 be object ; :: thesis:
A25: v2 is set by TARSKI:1;
assume A26: ( v1 <> v & v2 <> v ) ; :: thesis:
assume e DJoins v1,v2,G2 ; :: thesis:
then e DJoins v1,v2,G1 by A3, A19, A25, GLIB_006:70;
hence e DJoins v1,v2,G3 by A1, A26, Def4; :: thesis:

end;

take F = F; :: thesis:
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

proof

per cases ;

suppose G1 .edgesBetween (W,{v}) <> {} ; :: thesis:

hence dom f = W by FUNCT_2:def 1; :: thesis:

end;

suppose A29: G1 .edgesBetween (W,{v}) = {} ; :: thesis:

then dom f = {} ;
hence dom f = W by A29, A1, Lm12; :: thesis:

end;

end;

end;

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; :: thesis:
thus F misses the_Edges_of G3 by A5, XBOOLE_1:63; :: thesis:
thus the_Edges_of G2 = (the_Edges_of G3) \/ F by A16; :: thesis:
let v1 be object ; :: thesis:
assume A30: v1 in V1 ; :: thesis:
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; :: thesis:
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; :: thesis:
then A33: e1 in the_Edges_of G2 by A16, XBOOLE_0:def 3;
thus e1 Joins v1,v,G2 :: thesis:

proof

reconsider e3 = e1 as set by TARSKI:1;
A34: ( ( (the_Source_of G1) . e1 = v1 & (the_Target_of G1) . e1 = v ) or ( (the_Source_of G1) . e1 = v & (the_Target_of G1) . e1 = v1 ) ) by A31, GLIB_000:def 13;
( (the_Source_of G1) . e3 = (the_Source_of G2) . e3 & (the_Target_of G1) . e3 = (the_Target_of G2) . e3 ) by A33, GLIB_000:def 32;
hence e1 Joins v1,v,G2 by A33, GLIB_000:def 13, A34; :: thesis:

end;

let e2 be object ; :: thesis:
assume A35: e2 Joins v1,v,G2 ; :: thesis:
( v1 is set & v is set ) by TARSKI:1;
hence e1 = e2 by A32, A35, GLIB_000:72; :: thesis:

end;

G2 is Supergraph of G3

proof

A36: the_Vertices_of G3 c= the_Vertices_of G2 by A17, XBOOLE_1:7;
A37: the_Edges_of G3 c= the_Edges_of G2 by A16, XBOOLE_1:7;

now :: thesis:

let e be set ; :: thesis:
assume A38: e in the_Edges_of G3 ; :: thesis:
then A39: e in the_Edges_of G2 by A37;
thus (the_Source_of G3) . e = (the_Source_of G1) . e by A38, GLIB_006:def 9
.= (the_Source_of G2) . e by A39, GLIB_000:def 32 ; :: thesis:
thus (the_Target_of G3) . e = (the_Target_of G1) . e by A38, GLIB_006:def 9
.= (the_Target_of G2) . e by A39, GLIB_000:def 32 ; :: thesis:

end;

hence G2 is Supergraph of G3 by A36, A37, GLIB_006:def 9; :: thesis:

end;

hence G2 is addAdjVertexAll of G3,v,V1 by A4, A17, Def4; :: thesis: