A1: rng (e .--> v1) = rng ({e} --> v1) by FUNCOP_1:def 9
.= {v1} by FUNCOP_1:8 ;
A2: rng (e .--> v2) = rng ({e} --> v2) by FUNCOP_1:def 9
.= {v2} by FUNCOP_1:8 ;
A3: dom (e .--> v1) = dom ({e} --> v1) by FUNCOP_1:def 9
.= {e} ;
A4: dom (e .--> v2) = dom ({e} --> v2) by FUNCOP_1:def 9
.= {e} ;

hereby :: thesis: ( ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G implies ex b₁ being Supergraph of G st
( the_Vertices_of b₁ = (the_Vertices_of G) \/ {v1} & the_Edges_of b₁ = (the_Edges_of G) \/ {e} & the_Source_of b₁ = (the_Source_of G) +* (e .--> v1) & the_Target_of b₁ = (the_Target_of G) +* (e .--> v2) ) ) & ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( 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 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 )

proof

let e1 be set ; :: thesis: ( e1 in the_Edges_of G implies ( (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 ) )
assume e1 in the_Edges_of G ; :: thesis: ( (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 A14: ( not e1 in dom (e .--> v1) & not e1 in dom (e .--> v2) ) by A7, TARSKI:def 1;
thus (the_Source_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 = ((the_Source_of G) +* (e .--> v1)) . e1
.= (the_Source_of G) . e1 by A14, FUNCT_4:11 ; :: thesis: (the_Target_of G) . e1 = (the_Target_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1
thus (the_Target_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 = ((the_Target_of G) +* (e .--> v2)) . e1
.= (the_Target_of G) . e1 by A14, FUNCT_4:11 ; :: thesis: verum
thus verum ; :: thesis: verum

end;

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

end;

hereby :: thesis: ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( 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 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 )

proof

let e1 be set ; :: thesis: ( e1 in the_Edges_of G implies ( (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 ) )
assume e1 in the_Edges_of G ; :: thesis: ( (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 A22: ( not e1 in dom (e .--> v1) & not e1 in dom (e .--> v2) ) by A15, TARSKI:def 1;
thus (the_Source_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 = ((the_Source_of G) +* (e .--> v1)) . e1
.= (the_Source_of G) . e1 by A22, FUNCT_4:11 ; :: thesis: (the_Target_of G) . e1 = (the_Target_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1
thus (the_Target_of (createGraph (V1,((the_Edges_of G) \/ {e}),S1,T1))) . e1 = ((the_Target_of G) +* (e .--> v2)) . e1
.= (the_Target_of G) . e1 by A22, FUNCT_4:11 ; :: thesis: verum
thus verum ; :: thesis: verum

end;

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

end;

assume ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( 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