let G3 be _Graph; :: thesis:
let v be object ; :: thesis:
let V be set ; :: thesis:
let v1 be Vertex of G3; :: thesis:
let e be object ; :: thesis:
let G2 be addAdjVertexAll of G3,v,V; :: thesis:
assume that
A1: ( V c= the_Vertices_of G3 & not v in the_Vertices_of G3 ) and
A2: ( not v1 in V & not e in the_Edges_of G2 ) ; :: thesis:
consider E being set such that
A3: ( card V = card E & E misses the_Edges_of G3 & the_Edges_of G2 = (the_Edges_of G3) \/ E ) and
A4: for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G2 & ( for e2 being object st e2 Joins v1,v,G2 holds
e1 = e2 ) ) by A1, Def4;
consider f being Function such that
A5: ( f is one-to-one & dom f = E & rng f = V ) by WELLORD2:def 4, A3, CARD_1:5;
set f1 = f +* (e .--> v1);
reconsider E1 = E \/ {e}, V1 = V \/ {v1} as set ;
A6: dom (f +* (e .--> v1)) = (dom f) \/ (dom (e .--> v1)) by FUNCT_4:def 1
.= (dom f) \/ (dom ({e} --> v1)) by FUNCOP_1:def 9
.= E1 by A5 ;
( e is set & v1 is set ) by TARSKI:1;
then A7: rng (e .--> v1) = {v1} by FUNCOP_1:88;
then A8: (rng f) \/ (rng (e .--> v1)) = V \/ {v1} by A5;
(rng f) /\ (rng (e .--> v1)) = {}

proof

assume A9: (rng f) /\ (rng (e .--> v1)) <> {} ; :: thesis:
set x = the Element of (rng f) /\ (rng (e .--> v1));
( the Element of (rng f) /\ (rng (e .--> v1)) in V & the Element of (rng f) /\ (rng (e .--> v1)) in {v1} ) by XBOOLE_0:def 4, A5, A7, A9;
hence contradiction by A2, TARSKI:def 1; :: thesis:

end;

then A10: f +* (e .--> v1) is one-to-one by A5, XBOOLE_0:def 7, FUNCT_4:92;
for w being object st w in (rng f) \/ (rng (e .--> v1)) holds
w in rng (f +* (e .--> v1))

proof

let w be object ; :: thesis:
assume w in (rng f) \/ (rng (e .--> v1)) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose w in rng f ; :: thesis:

then consider x being object such that
A11: ( x in dom f & w = f . x ) by FUNCT_1:def 3;
x in E by A5, A11;
then x <> e by A2, A3, XBOOLE_0:def 3;
then A13: (f +* (e .--> v1)) . x = w by A11, FUNCT_4:83;
x in E1 by A5, A11, XBOOLE_0:def 3;
hence w in rng (f +* (e .--> v1)) by A6, A13, FUNCT_1:def 3; :: thesis:

end;

suppose w in rng (e .--> v1) ; :: thesis:

hence w in rng (f +* (e .--> v1)) by FUNCT_4:18, TARSKI:def 3; :: thesis:

end;

end;

end;

then A14: (rng f) \/ (rng (e .--> v1)) c= rng (f +* (e .--> v1)) by TARSKI:def 3;
rng (f +* (e .--> v1)) c= (rng f) \/ (rng (e .--> v1)) by FUNCT_4:17;
then rng (f +* (e .--> v1)) = (rng f) \/ (rng (e .--> v1)) by A14, XBOOLE_0:def 10;
then A15: card E1 = card V1 by A8, A10, A6, WELLORD2:def 4, CARD_1:5;
A16: (the_Edges_of G2) /\ {e} = {} by A2, ZFMISC_1:50, XBOOLE_0:def 7;
the_Edges_of G3 c= the_Edges_of G2 by GLIB_006:def 9;
then (the_Edges_of G3) /\ {e} c= (the_Edges_of G2) /\ {e} by XBOOLE_1:26;
then A17: (the_Edges_of G3) /\ {e} = {} by A16;
(the_Edges_of G3) /\ E1 = (the_Edges_of G3) /\ {e} by XBOOLE_1:78, A3;
then A18: E1 misses the_Edges_of G3 by A17, XBOOLE_0:def 7;
A19: (the_Edges_of G3) \/ E1 = (the_Edges_of G2) \/ {e} by A3, XBOOLE_1:4;
( v is Vertex of G2 & v1 is Vertex of G3 ) by A1, Th50;
then A20: ( v in the_Vertices_of G2 & v1 is Vertex of G2 ) by GLIB_006:68;
A21: V1 c= the_Vertices_of G3 by A1, XBOOLE_1:8;
let G1 be _Graph; :: thesis:
assume ( G1 is addEdge of G2,v1,e,v or G1 is addEdge of G2,v,e,v1 ) ; :: thesis:

per cases ;

suppose A22: G1 is addEdge of G2,v1,e,v ; :: thesis:

then A23: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ {e} & the_Source_of G1 = (the_Source_of G2) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G2) +* (e .--> v) ) by A20, A2, GLIB_006:def 11;
A24: G1 is Supergraph of G3 by A22, GLIB_006:62;

now :: thesis:

thus the_Vertices_of G1 = (the_Vertices_of G3) \/ {v} by A23, A1, Def4; :: thesis:

hereby :: thesis:

let e3 be object ; :: thesis:
thus not e3 Joins v,v,G1 :: thesis:

proof

assume A25: e3 Joins v,v,G1 ; :: thesis:

per cases by A22, GLIB_006:72;

suppose e3 Joins v,v,G2 ; :: thesis:

hence contradiction by A1, Def4; :: thesis:

end;

suppose not e3 in the_Edges_of G2 ; :: thesis:

then v1 = v by A2, A20, A22, A25, GLIB_006:107;
hence contradiction by A1; :: thesis:

end;

end;

end;

let v3 be object ; :: thesis:
thus ( not v3 in V1 implies not e3 Joins v3,v,G1 ) :: thesis:

proof

assume not v3 in V1 ; :: thesis:
then A26: ( not v3 in V & not v3 in {v1} ) by XBOOLE_0:def 3;
assume A27: e3 Joins v3,v,G1 ; :: thesis:

per cases by A22, GLIB_006:72;

suppose e3 Joins v3,v,G2 ; :: thesis:

hence contradiction by A1, A26, Def4; :: thesis:

end;

suppose not e3 in the_Edges_of G2 ; :: thesis:

per cases by A2, A20, A22, A27, GLIB_006:107;

suppose ( v3 = v1 & v = v ) ; :: thesis:

hence contradiction by A26, TARSKI:def 1; :: thesis:

end;

suppose ( v3 = v & v = v1 ) ; :: thesis:

hence contradiction by A1; :: thesis:

end;

end;

end;

end;

end;

let v2 be object ; :: thesis:
assume A28: ( v3 <> v & v2 <> v & e3 DJoins v3,v2,G1 ) ; :: thesis:

per cases by A24, GLIB_006:71;

suppose e3 DJoins v3,v2,G3 ; :: thesis:

hence e3 DJoins v3,v2,G3 ; :: thesis:

end;

suppose not e3 in the_Edges_of G3 ; :: thesis:

per cases by A22, A28, GLIB_006:71;

suppose e3 DJoins v3,v2,G2 ; :: thesis:

hence e3 DJoins v3,v2,G3 by A28, A1, Def4; :: thesis:

end;

suppose A29: not e3 in the_Edges_of G2 ; :: thesis:

e3 Joins v3,v2,G1 by A28, GLIB_000:16;
then ( ( v3 = v1 & v2 = v ) or ( v3 = v & v2 = v1 ) ) by A2, A20, A22, A29, GLIB_006:107;
hence e3 DJoins v3,v2,G3 by A28; :: thesis:

end;

end;

end;

end;

end;

take E1 = E1; :: thesis:
thus card V1 = card E1 by A15; :: thesis:
thus E1 misses the_Edges_of G3 by A18; :: thesis:
thus the_Edges_of G1 = (the_Edges_of G3) \/ E1 by A19, A23; :: thesis:
let v3 be object ; :: thesis:
assume A30: v3 in V1 ; :: thesis:
thus ex e1 being object st
( e1 in E1 & e1 Joins v3,v,G1 & ( for e2 being object st e2 Joins v3,v,G1 holds
e1 = e2 ) ) :: thesis:

proof

per cases by A30, XBOOLE_0:def 3;

suppose A31: v3 in V ; :: thesis:

then consider e1 being object such that
A32: ( e1 in E & e1 Joins v3,v,G2 ) and
A33: for e2 being object st e2 Joins v3,v,G2 holds
e1 = e2 by A4;
take e1 ; :: thesis:
thus e1 in E1 by A32, XBOOLE_0:def 3; :: thesis:
( v3 is set & v is set ) by TARSKI:1;
hence e1 Joins v3,v,G1 by A22, A32, GLIB_006:70; :: thesis:
let e2 be object ; :: thesis:
assume A34: e2 Joins v3,v,G1 ; :: thesis:

per cases by A22, GLIB_006:72;

suppose e2 Joins v3,v,G2 ; :: thesis:

hence e1 = e2 by A33; :: thesis:

end;

suppose not e2 in the_Edges_of G2 ; :: thesis:

per cases by A2, A20, A22, A34, GLIB_006:107;

suppose ( v3 = v1 & v = v ) ; :: thesis:

hence e1 = e2 by A2, A31; :: thesis:

end;

suppose ( v3 = v & v = v1 ) ; :: thesis:

hence e1 = e2 by A1; :: thesis:

end;

end;

end;

end;

end;

suppose v3 in {v1} ; :: thesis:

then A35: v3 = v1 by TARSKI:def 1;
take e ; :: thesis:
e in {e} by TARSKI:def 1;
hence e in E1 by XBOOLE_0:def 3; :: thesis:
e DJoins v1,v,G1 by A2, A20, A22, GLIB_006:105;
hence e Joins v3,v,G1 by A35, GLIB_000:16; :: thesis:
let e2 be object ; :: thesis:
assume A36: e2 Joins v3,v,G1 ; :: thesis:

per cases by A22, GLIB_006:72, A35;

suppose e2 Joins v1,v,G2 ; :: thesis:

hence e = e2 by A2, A1, Def4; :: thesis:

end;

suppose not e2 in the_Edges_of G2 ; :: thesis:

hence e = e2 by A2, A20, A22, A36, GLIB_006:106; :: thesis:

end;

end;

end;

end;

end;

end;

hence G1 is addAdjVertexAll of G3,v,V \/ {v1} by A24, A21, A1, Def4; :: thesis:

end;

suppose A37: G1 is addEdge of G2,v,e,v1 ; :: thesis:

then A38: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ {e} & the_Source_of G1 = (the_Source_of G2) +* (e .--> v) & the_Target_of G1 = (the_Target_of G2) +* (e .--> v1) ) by A20, A2, GLIB_006:def 11;
A39: G1 is Supergraph of G3 by A37, GLIB_006:62;

now :: thesis:

thus the_Vertices_of G1 = (the_Vertices_of G3) \/ {v} by A1, A38, Def4; :: thesis:

hereby :: thesis:

let e3 be object ; :: thesis:
thus not e3 Joins v,v,G1 :: thesis:

proof

assume A40: e3 Joins v,v,G1 ; :: thesis:

per cases by A37, GLIB_006:72;

suppose e3 Joins v,v,G2 ; :: thesis:

hence contradiction by A1, Def4; :: thesis:

end;

suppose not e3 in the_Edges_of G2 ; :: thesis:

then v1 = v by A2, A20, A37, A40, GLIB_006:107;
hence contradiction by A1; :: thesis:

end;

end;

end;

let v3 be object ; :: thesis:
thus ( not v3 in V1 implies not e3 Joins v3,v,G1 ) :: thesis:

proof

assume not v3 in V1 ; :: thesis:
then A41: ( not v3 in V & not v3 in {v1} ) by XBOOLE_0:def 3;
assume A42: e3 Joins v3,v,G1 ; :: thesis:

per cases by A37, GLIB_006:72;

suppose e3 Joins v3,v,G2 ; :: thesis:

hence contradiction by A1, A41, Def4; :: thesis:

end;

suppose not e3 in the_Edges_of G2 ; :: thesis:

per cases by A2, A20, A37, A42, GLIB_006:107;

suppose ( v3 = v & v = v1 ) ; :: thesis:

hence contradiction by A1; :: thesis:

end;

suppose ( v3 = v1 & v = v ) ; :: thesis:

hence contradiction by A41, TARSKI:def 1; :: thesis:

end;

end;

end;

end;

end;

let v2 be object ; :: thesis:
assume A43: ( v3 <> v & v2 <> v & e3 DJoins v3,v2,G1 ) ; :: thesis:

per cases by A39, GLIB_006:71;

suppose e3 DJoins v3,v2,G3 ; :: thesis:

hence e3 DJoins v3,v2,G3 ; :: thesis:

end;

suppose not e3 in the_Edges_of G3 ; :: thesis:

per cases by A37, A43, GLIB_006:71;

suppose e3 DJoins v3,v2,G2 ; :: thesis:

hence e3 DJoins v3,v2,G3 by A43, A1, Def4; :: thesis:

end;

suppose A44: not e3 in the_Edges_of G2 ; :: thesis:

e3 Joins v3,v2,G1 by A43, GLIB_000:16;
then ( ( v3 = v & v2 = v1 ) or ( v3 = v1 & v2 = v ) ) by A2, A20, A37, A44, GLIB_006:107;
hence e3 DJoins v3,v2,G3 by A43; :: thesis:

end;

end;

end;

end;

end;

take E1 = E1; :: thesis:
thus card V1 = card E1 by A15; :: thesis:
thus E1 misses the_Edges_of G3 by A18; :: thesis:
thus the_Edges_of G1 = (the_Edges_of G3) \/ E1 by A19, A38; :: thesis:
let v3 be object ; :: thesis:
assume A45: v3 in V1 ; :: thesis:
thus ex e1 being object st
( e1 in E1 & e1 Joins v3,v,G1 & ( for e2 being object st e2 Joins v3,v,G1 holds
e1 = e2 ) ) :: thesis:

proof

per cases by A45, XBOOLE_0:def 3;

suppose A46: v3 in V ; :: thesis:

then consider e1 being object such that
A47: ( e1 in E & e1 Joins v3,v,G2 ) and
A48: for e2 being object st e2 Joins v3,v,G2 holds
e1 = e2 by A4;
take e1 ; :: thesis:
thus e1 in E1 by A47, XBOOLE_0:def 3; :: thesis:
( v3 is set & v is set ) by TARSKI:1;
hence e1 Joins v3,v,G1 by A37, A47, GLIB_006:70; :: thesis:
let e2 be object ; :: thesis:
assume A49: e2 Joins v3,v,G1 ; :: thesis:

per cases by A37, GLIB_006:72;

suppose e2 Joins v3,v,G2 ; :: thesis:

hence e1 = e2 by A48; :: thesis:

end;

suppose not e2 in the_Edges_of G2 ; :: thesis:

per cases by A2, A20, A37, A49, GLIB_006:107;

suppose ( v3 = v & v = v1 ) ; :: thesis:

hence e1 = e2 by A1; :: thesis:

end;

suppose ( v3 = v1 & v = v ) ; :: thesis:

hence e1 = e2 by A2, A46; :: thesis:

end;

end;

end;

end;

end;

suppose v3 in {v1} ; :: thesis:

then A50: v3 = v1 by TARSKI:def 1;
take e ; :: thesis:
e in {e} by TARSKI:def 1;
hence e in E1 by XBOOLE_0:def 3; :: thesis:
e DJoins v,v1,G1 by A2, A20, A37, GLIB_006:105;
hence e Joins v3,v,G1 by A50, GLIB_000:16; :: thesis:
let e2 be object ; :: thesis:
assume A51: e2 Joins v3,v,G1 ; :: thesis:

per cases by A50, A37, GLIB_006:72;

suppose e2 Joins v1,v,G2 ; :: thesis:

hence e = e2 by A2, A1, Def4; :: thesis:

end;

suppose not e2 in the_Edges_of G2 ; :: thesis:

hence e = e2 by A2, A20, A37, A51, GLIB_006:106; :: thesis:

end;

end;

end;

end;

end;

end;

hence G1 is addAdjVertexAll of G3,v,V \/ {v1} by A39, A21, A1, Def4; :: thesis:

end;

end;