hereby :: thesis: ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ex b₁ being Supergraph of G st b₁ == G )

assume A1: ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis: ex G1 being Supergraph of G st
( the_Vertices_of G1 = (the_Vertices_of G) \/ {v} & the_Edges_of G1 = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of G1 = (the_Source_of G) +* ((V --> (the_Edges_of G)) --> v) & the_Target_of G1 = (the_Target_of G) +* (pr1 (V,{(the_Edges_of G)})) )
set V1 = (the_Vertices_of G) \/ {v};
reconsider V1 = (the_Vertices_of G) \/ {v} as non empty set ;
set E1 = (the_Edges_of G) \/ (V --> (the_Edges_of G));
set S1 = (the_Source_of G) +* ((V --> (the_Edges_of G)) --> v);
A2: dom ((the_Source_of G) +* ((V --> (the_Edges_of G)) --> v)) = (dom (the_Source_of G)) \/ (dom ((V --> (the_Edges_of G)) --> v)) by FUNCT_4:def 1
.= (the_Edges_of G) \/ (dom ((V --> (the_Edges_of G)) --> v)) by FUNCT_2:def 1
.= (the_Edges_of G) \/ (V --> (the_Edges_of G)) ;
A3: (rng (the_Source_of G)) \/ (rng ((V --> (the_Edges_of G)) --> v)) c= V1 by XBOOLE_1:13;
rng ((the_Source_of G) +* ((V --> (the_Edges_of G)) --> v)) c= (rng (the_Source_of G)) \/ (rng ((V --> (the_Edges_of G)) --> v)) by FUNCT_4:17;
then reconsider S1 = (the_Source_of G) +* ((V --> (the_Edges_of G)) --> v) as Function of ((the_Edges_of G) \/ (V --> (the_Edges_of G))),V1 by A2, FUNCT_2:2, A3, XBOOLE_1:1;
set T1 = (the_Target_of G) +* (pr1 (V,{(the_Edges_of G)}));
A4: dom ((the_Target_of G) +* (pr1 (V,{(the_Edges_of G)}))) = (dom (the_Target_of G)) \/ (dom (pr1 (V,{(the_Edges_of G)}))) by FUNCT_4:def 1
.= (the_Edges_of G) \/ (dom (pr1 (V,{(the_Edges_of G)}))) by FUNCT_2:def 1
.= (the_Edges_of G) \/ [:V,{(the_Edges_of G)}:] by FUNCT_3:def 4
.= (the_Edges_of G) \/ (V --> (the_Edges_of G)) by FUNCOP_1:def 2 ;
rng (pr1 (V,{(the_Edges_of G)})) c= the_Vertices_of G by A1, XBOOLE_1:1;
then (rng (the_Target_of G)) \/ (rng (pr1 (V,{(the_Edges_of G)}))) c= the_Vertices_of G by XBOOLE_1:8;
then A5: (rng (the_Target_of G)) \/ (rng (pr1 (V,{(the_Edges_of G)}))) c= V1 by XBOOLE_1:10;
rng ((the_Target_of G) +* (pr1 (V,{(the_Edges_of G)}))) c= (rng (the_Target_of G)) \/ (rng (pr1 (V,{(the_Edges_of G)}))) by FUNCT_4:17;
then reconsider T1 = (the_Target_of G) +* (pr1 (V,{(the_Edges_of G)})) as Function of ((the_Edges_of G) \/ (V --> (the_Edges_of G))),V1 by A4, FUNCT_2:2, A5, XBOOLE_1:1;
set G1 = createGraph (V1,((the_Edges_of G) \/ (V --> (the_Edges_of G))),S1,T1);
( the_Vertices_of G c= V1 & the_Edges_of G c= (the_Edges_of G) \/ (V --> (the_Edges_of G)) ) by XBOOLE_1:7;
then A6: ( the_Vertices_of G c= the_Vertices_of (createGraph (V1,((the_Edges_of G) \/ (V --> (the_Edges_of G))),S1,T1)) & the_Edges_of G c= the_Edges_of (createGraph (V1,((the_Edges_of G) \/ (V --> (the_Edges_of G))),S1,T1)) ) ;
for e being set st e in the_Edges_of G holds
( (the_Source_of G) . e = (the_Source_of (createGraph (V1,((the_Edges_of G) \/ (V --> (the_Edges_of G))),S1,T1))) . e & (the_Target_of G) . e = (the_Target_of (createGraph (V1,((the_Edges_of G) \/ (V --> (the_Edges_of G))),S1,T1))) . e )

proof

let e be set ; :: thesis: ( e in the_Edges_of G implies ( (the_Source_of G) . e = (the_Source_of (createGraph (V1,((the_Edges_of G) \/ (V --> (the_Edges_of G))),S1,T1))) . e & (the_Target_of G) . e = (the_Target_of (createGraph (V1,((the_Edges_of G) \/ (V --> (the_Edges_of G))),S1,T1))) . e ) )
assume A7: e in the_Edges_of G ; :: thesis: ( (the_Source_of G) . e = (the_Source_of (createGraph (V1,((the_Edges_of G) \/ (V --> (the_Edges_of G))),S1,T1))) . e & (the_Target_of G) . e = (the_Target_of (createGraph (V1,((the_Edges_of G) \/ (V --> (the_Edges_of G))),S1,T1))) . e )
then e in dom (the_Source_of G) by FUNCT_2:def 1;
then A8: e in (dom (the_Source_of G)) \/ (dom ((V --> (the_Edges_of G)) --> v)) by XBOOLE_1:7, TARSKI:def 3;
a9: (the_Edges_of G) /\ (V --> (the_Edges_of G)) = {} by Lm6;
then A9: not e in V --> (the_Edges_of G) by A7, Lm7;
not e in dom ((V --> (the_Edges_of G)) --> v) by A7, Lm7, a9;
then A10: S1 . e = (the_Source_of G) . e by A8, FUNCT_4:def 1;
e in dom (the_Target_of G) by A7, FUNCT_2:def 1;
then A11: e in (dom (the_Target_of G)) \/ (dom (pr1 (V,{(the_Edges_of G)}))) by XBOOLE_1:7, TARSKI:def 3;
not e in [:V,{(the_Edges_of G)}:] by A9, FUNCOP_1:def 2;
then not e in dom (pr1 (V,{(the_Edges_of G)})) ;
then T1 . e = (the_Target_of G) . e by A11, FUNCT_4:def 1;
hence ( (the_Source_of G) . e = (the_Source_of (createGraph (V1,((the_Edges_of G) \/ (V --> (the_Edges_of G))),S1,T1))) . e & (the_Target_of G) . e = (the_Target_of (createGraph (V1,((the_Edges_of G) \/ (V --> (the_Edges_of G))),S1,T1))) . e ) by A10; :: thesis: verum

end;

then reconsider G1 = createGraph (V1,((the_Edges_of G) \/ (V --> (the_Edges_of G))),S1,T1) as Supergraph of G by A6, GLIB_006:def 9;
take G1 = G1; :: thesis: ( the_Vertices_of G1 = (the_Vertices_of G) \/ {v} & the_Edges_of G1 = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of G1 = (the_Source_of G) +* ((V --> (the_Edges_of G)) --> v) & the_Target_of G1 = (the_Target_of G) +* (pr1 (V,{(the_Edges_of G)})) )
thus ( the_Vertices_of G1 = (the_Vertices_of G) \/ {v} & the_Edges_of G1 = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of G1 = (the_Source_of G) +* ((V --> (the_Edges_of G)) --> v) & the_Target_of G1 = (the_Target_of G) +* (pr1 (V,{(the_Edges_of G)})) ) ; :: thesis: verum

end;

assume ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis: ex b₁ being Supergraph of G st b₁ == G
reconsider G1 = G as Supergraph of G by GLIB_006:61;
take G1 ; :: thesis: G1 == G
thus G1 == G ; :: thesis: verum