hereby ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ex b1 being Supergraph of G st b1 == G )
assume A1:
(
V c= the_Vertices_of G & not
v in the_Vertices_of G )
;
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) +* (pr1 (V,{(the_Edges_of G)})) & the_Target_of G1 = (the_Target_of G) +* ((V --> (the_Edges_of G)) --> v) )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 T1 =
(the_Target_of G) +* ((V --> (the_Edges_of G)) --> v);
A2:
dom ((the_Target_of G) +* ((V --> (the_Edges_of G)) --> v)) =
(dom (the_Target_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_Target_of G)) \/ (rng ((V --> (the_Edges_of G)) --> v)) c= V1
by XBOOLE_1:13;
rng ((the_Target_of G) +* ((V --> (the_Edges_of G)) --> v)) c= (rng (the_Target_of G)) \/ (rng ((V --> (the_Edges_of G)) --> v))
by FUNCT_4:17;
then reconsider T1 =
(the_Target_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 S1 =
(the_Source_of G) +* (pr1 (V,{(the_Edges_of G)}));
A4:
dom ((the_Source_of G) +* (pr1 (V,{(the_Edges_of G)}))) =
(dom (the_Source_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_Source_of G)) \/ (rng (pr1 (V,{(the_Edges_of G)}))) c= the_Vertices_of G
by XBOOLE_1:8;
then A5:
(rng (the_Source_of G)) \/ (rng (pr1 (V,{(the_Edges_of G)}))) c= V1
by XBOOLE_1:10;
rng ((the_Source_of G) +* (pr1 (V,{(the_Edges_of G)}))) c= (rng (the_Source_of G)) \/ (rng (pr1 (V,{(the_Edges_of G)})))
by FUNCT_4:17;
then reconsider S1 =
(the_Source_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 ;
( 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
;
( (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_Target_of G)
by FUNCT_2:def 1;
then A8:
e in (dom (the_Target_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:
T1 . e = (the_Target_of G) . e
by A8, FUNCT_4:def 1;
e in dom (the_Source_of G)
by A7, FUNCT_2:def 1;
then A11:
e in (dom (the_Source_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
S1 . e = (the_Source_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;
verum
end; then reconsider G1 =
createGraph (
V1,
((the_Edges_of G) \/ (V --> (the_Edges_of G))),
S1,
T1) as
Supergraph of
G by GLIB_006:def 9, A6;
take G1 =
G1;
( 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) +* (pr1 (V,{(the_Edges_of G)})) & the_Target_of G1 = (the_Target_of G) +* ((V --> (the_Edges_of G)) --> v) )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) +* (pr1 (V,{(the_Edges_of G)})) &
the_Target_of G1 = (the_Target_of G) +* ((V --> (the_Edges_of G)) --> v) )
;
verum
end;
assume
( not V c= the_Vertices_of G or v in the_Vertices_of G )
; ex b1 being Supergraph of G st b1 == G
reconsider G1 = G as Supergraph of G by GLIB_006:61;
take
G1
; G1 == G
thus
G1 == G
; verum