hereby :: thesis: ( ( not v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) implies ex b₁ being Supergraph of G st b₁ == G )

assume A1: ( 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 & 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;
set E1 = (the_Edges_of G) \/ {e};
A2: rng (e .--> v1) = rng ({e} --> v1) by FUNCOP_1:def 9
.= {v1} by FUNCOP_1:8 ;
A3: rng (e .--> v2) = rng ({e} --> v2) by FUNCOP_1:def 9
.= {v2} by FUNCOP_1:8 ;
A4: dom (e .--> v1) = dom ({e} --> v1) by FUNCOP_1:def 9
.= {e} ;
A5: dom (e .--> v2) = dom ({e} --> v2) by FUNCOP_1:def 9
.= {e} ;
set S1 = (the_Source_of G) +* (e .--> v1);
A6: 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, A4 ;
(rng (the_Source_of G)) \/ {v1} c= (the_Vertices_of G) \/ {v1} by XBOOLE_1:9;
then A7: (rng (the_Source_of G)) \/ (rng (e .--> v1)) c= the_Vertices_of G by A1, A2, ZFMISC_1:40;
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}),(the_Vertices_of G) by A6, A7, FUNCT_2:2, XBOOLE_1:1;
set T1 = (the_Target_of G) +* (e .--> v2);
A8: 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, A5 ;
(rng (the_Target_of G)) \/ {v2} c= (the_Vertices_of G) \/ {v2} by XBOOLE_1:9;
then A9: (rng (the_Target_of G)) \/ (rng (e .--> v2)) c= the_Vertices_of G by A1, A3, ZFMISC_1:40;
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}),(the_Vertices_of G) by A8, A9, FUNCT_2:2, XBOOLE_1:1;
set G1 = createGraph ((the_Vertices_of G),((the_Edges_of G) \/ {e}),S1,T1);
for e1 being set st e1 in the_Edges_of G holds
( (the_Source_of G) . e1 = (the_Source_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ {e}),S1,T1))) . e1 & (the_Target_of G) . e1 = (the_Target_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ {e}),S1,T1))) . e1 )

proof

let e1 be set ; :: thesis: ( e1 in the_Edges_of G implies ( (the_Source_of G) . e1 = (the_Source_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ {e}),S1,T1))) . e1 & (the_Target_of G) . e1 = (the_Target_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ {e}),S1,T1))) . e1 ) )
assume e1 in the_Edges_of G ; :: thesis: ( (the_Source_of G) . e1 = (the_Source_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ {e}),S1,T1))) . e1 & (the_Target_of G) . e1 = (the_Target_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ {e}),S1,T1))) . e1 )
then A12: ( not e1 in dom (e .--> v1) & not e1 in dom (e .--> v2) ) by A1, TARSKI:def 1;
thus (the_Source_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ {e}),S1,T1))) . e1 = ((the_Source_of G) +* (e .--> v1)) . e1
.= (the_Source_of G) . e1 by A12, FUNCT_4:11 ; :: thesis: (the_Target_of G) . e1 = (the_Target_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ {e}),S1,T1))) . e1
thus (the_Target_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ {e}),S1,T1))) . e1 = ((the_Target_of G) +* (e .--> v2)) . e1
.= (the_Target_of G) . e1 by A12, FUNCT_4:11 ; :: thesis: verum
thus verum ; :: thesis: verum

end;

then reconsider G1 = createGraph ((the_Vertices_of G),((the_Edges_of G) \/ {e}),S1,T1) as Supergraph of G by Def9, XBOOLE_1:7;
take G1 = G1; :: thesis: ( the_Vertices_of G1 = the_Vertices_of G & 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 & 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

end;

assume ( not v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) ; :: thesis: ex b₁ being Supergraph of G st b₁ == G
reconsider G1 = G as Supergraph of G by Th65;
take G1 ; :: thesis: G1 == G
thus G1 == G ; :: thesis: verum