assume A7: ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis: ex G1 being Supergraph of G st
( the_Vertices_of G1 = (the_Vertices_of G) \/ {v2} & the_Edges_of G1 = (the_Edges_of G) \/ {e} & the_Source_of G1 = (the_Source_of G) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G) +* (e .--> v2) )
set V1 = (the_Vertices_of G) \/ {v2};
reconsider V1 = (the_Vertices_of G) \/ {v2} as non empty set ;
set E1 = (the_Edges_of G) \/ {e};
set S1 = (the_Source_of G) +* (e .--> v1);
A8: dom ((the_Source_of G) +* (e .--> v1)) = (dom (the_Source_of G)) \/ (dom (e .--> v1)) by FUNCT_4:def 1
.= (the_Edges_of G) \/ {e} by FUNCT_2:def 1, A3 ;
A9: the_Vertices_of G c= V1 by XBOOLE_1:7;
(rng (the_Source_of G)) \/ {v1} c= (the_Vertices_of G) \/ {v1} by XBOOLE_1:9;
then (rng (the_Source_of G)) \/ {v1} c= the_Vertices_of G by A7, ZFMISC_1:40;
then A10: (rng (the_Source_of G)) \/ (rng (e .--> v1)) c= V1 by A1, A9, XBOOLE_1:1;
rng ((the_Source_of G) +* (e .--> v1)) c= (rng (the_Source_of G)) \/ (rng (e .--> v1)) by FUNCT_4:17;
then reconsider S1 = (the_Source_of G) +* (e .--> v1) as Function of ((the_Edges_of G) \/ {e}),V1 by A8, A10, FUNCT_2:2, XBOOLE_1:1;
set T1 = (the_Target_of G) +* (e .--> v2);
A11: dom ((the_Target_of G) +* (e .--> v2)) = (dom (the_Target_of G)) \/ (dom (e .--> v2)) by FUNCT_4:def 1
.= (the_Edges_of G) \/ {e} by FUNCT_2:def 1, A4 ;
A12: (rng (the_Target_of G)) \/ (rng (e .--> v2)) c= V1 by A2, XBOOLE_1:9;
rng ((the_Target_of G) +* (e .--> v2)) c= (rng (the_Target_of G)) \/ (rng (e .--> v2)) by FUNCT_4:17;
then reconsider T1 = (the_Target_of G) +* (e .--> v2) as Function of ((the_Edges_of G) \/ {e}),V1 by A11, A12, FUNCT_2:2, XBOOLE_1:1;
set G1 = createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1);
the_Edges_of G c= (the_Edges_of G) \/ {e} by XBOOLE_1:7;
then A13: ( the_Edges_of G c= the_Edges_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1)) & the_Vertices_of G c= the_Vertices_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1)) ) by A9;
for e1 being set st e1 in the_Edges_of G holds
( (the_Source_of G) . e1 = (the_Source_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 & (the_Target_of G) . e1 = (the_Target_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 ) then reconsider G1 = createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1) as Supergraph of G by A13, Def9;
take G1 = G1; :: thesis: ( the_Vertices_of G1 = (the_Vertices_of G) \/ {v2} & the_Edges_of G1 = (the_Edges_of G) \/ {e} & the_Source_of G1 = (the_Source_of G) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G) +* (e .--> v2) )
thus ( the_Vertices_of G1 = (the_Vertices_of G) \/ {v2} & the_Edges_of G1 = (the_Edges_of G) \/ {e} & the_Source_of G1 = (the_Source_of G) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G) +* (e .--> v2) ) ; :: thesis: verum

assume A15: ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis: ex G1 being Supergraph of G st
( the_Vertices_of G1 = (the_Vertices_of G) \/ {v1} & the_Edges_of G1 = (the_Edges_of G) \/ {e} & the_Source_of G1 = (the_Source_of G) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G) +* (e .--> v2) )
set V1 = (the_Vertices_of G) \/ {v1};
reconsider V1 = (the_Vertices_of G) \/ {v1} as non empty set ;
set E1 = (the_Edges_of G) \/ {e};
set S1 = (the_Source_of G) +* (e .--> v1);
A16: dom ((the_Source_of G) +* (e .--> v1)) = (dom (the_Source_of G)) \/ (dom (e .--> v1)) by FUNCT_4:def 1
.= (the_Edges_of G) \/ {e} by FUNCT_2:def 1, A3 ;
A17: the_Vertices_of G c= V1 by XBOOLE_1:7;
A18: (rng (the_Source_of G)) \/ (rng (e .--> v1)) c= V1 by A1, XBOOLE_1:9;
rng ((the_Source_of G) +* (e .--> v1)) c= (rng (the_Source_of G)) \/ (rng (e .--> v1)) by FUNCT_4:17;
then reconsider S1 = (the_Source_of G) +* (e .--> v1) as Function of ((the_Edges_of G) \/ {e}),V1 by A16, A18, FUNCT_2:2, XBOOLE_1:1;
set T1 = (the_Target_of G) +* (e .--> v2);
A19: dom ((the_Target_of G) +* (e .--> v2)) = (dom (the_Target_of G)) \/ (dom (e .--> v2)) by FUNCT_4:def 1
.= (the_Edges_of G) \/ {e} by FUNCT_2:def 1, A4 ;
(rng (the_Target_of G)) \/ {v2} c= (the_Vertices_of G) \/ {v2} by XBOOLE_1:9;
then (rng (the_Target_of G)) \/ {v2} c= the_Vertices_of G by A15, ZFMISC_1:40;
then A20: (rng (the_Target_of G)) \/ (rng (e .--> v2)) c= V1 by A2, A17, XBOOLE_1:1;
rng ((the_Target_of G) +* (e .--> v2)) c= (rng (the_Target_of G)) \/ (rng (e .--> v2)) by FUNCT_4:17;
then reconsider T1 = (the_Target_of G) +* (e .--> v2) as Function of ((the_Edges_of G) \/ {e}),V1 by A19, A20, FUNCT_2:2, XBOOLE_1:1;
set G1 = createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1);
the_Edges_of G c= (the_Edges_of G) \/ {e} by XBOOLE_1:7;
then A21: ( the_Edges_of G c= the_Edges_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1)) & the_Vertices_of G c= the_Vertices_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1)) ) by A17;
for e1 being set st e1 in the_Edges_of G holds
( (the_Source_of G) . e1 = (the_Source_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 & (the_Target_of G) . e1 = (the_Target_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 ) then reconsider G1 = createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1) as Supergraph of G by A21, Def9;
take G1 = G1; :: thesis: ( the_Vertices_of G1 = (the_Vertices_of G) \/ {v1} & the_Edges_of G1 = (the_Edges_of G) \/ {e} & the_Source_of G1 = (the_Source_of G) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G) +* (e .--> v2) )
thus ( the_Vertices_of G1 = (the_Vertices_of G) \/ {v1} & the_Edges_of G1 = (the_Edges_of G) \/ {e} & the_Source_of G1 = (the_Source_of G) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G) +* (e .--> v2) ) ; :: thesis: verum