hereby ( not V c= the_Vertices_of G implies ex b1 being Supergraph of G st b1 == G )
assume A1:
V c= the_Vertices_of G
;
ex H being Supergraph of G st
( the_Vertices_of H = the_Vertices_of G & ex E being set ex f being one-to-one Function st
( E misses the_Edges_of G & the_Edges_of H = (the_Edges_of G) \/ E & dom f = E & rng f = V & the_Source_of H = (the_Source_of G) +* f & the_Target_of H = (the_Target_of G) +* f ) )set E =
{ [(the_Edges_of G),v] where v is Vertex of G : v in V } ;
deffunc H1(
object )
-> object = $1
`2 ;
consider f being
Function such that A2:
(
dom f = { [(the_Edges_of G),v] where v is Vertex of G : v in V } & ( for
x being
object st
x in { [(the_Edges_of G),v] where v is Vertex of G : v in V } holds
f . x = H1(
x) ) )
from FUNCT_1:sch 3();
set s =
(the_Source_of G) +* f;
set t =
(the_Target_of G) +* f;
then A6:
rng f = V
by TARSKI:2;
A7:
dom ((the_Source_of G) +* f) =
(dom (the_Source_of G)) \/ (dom f)
by FUNCT_4:def 1
.=
(the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V }
by A2, FUNCT_2:def 1
;
A8:
dom ((the_Target_of G) +* f) =
(dom (the_Target_of G)) \/ (dom f)
by FUNCT_4:def 1
.=
(the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V }
by A2, FUNCT_2:def 1
;
A9:
the_Edges_of G misses { [(the_Edges_of G),v] where v is Vertex of G : v in V }
(
(rng (the_Source_of G)) \/ (rng f) c= (the_Vertices_of G) \/ V &
(rng (the_Target_of G)) \/ (rng f) c= (the_Vertices_of G) \/ V )
by A6, XBOOLE_1:9;
then A13:
(
(rng (the_Source_of G)) \/ (rng f) c= the_Vertices_of G &
(rng (the_Target_of G)) \/ (rng f) c= the_Vertices_of G )
by A1, XBOOLE_1:12;
(
rng ((the_Source_of G) +* f) c= (rng (the_Source_of G)) \/ (rng f) &
rng ((the_Target_of G) +* f) c= (rng (the_Target_of G)) \/ (rng f) )
by FUNCT_4:17;
then A14:
(
rng ((the_Source_of G) +* f) c= the_Vertices_of G &
rng ((the_Target_of G) +* f) c= the_Vertices_of G )
by A13, XBOOLE_1:1;
then reconsider s =
(the_Source_of G) +* f as
Function of
((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),
(the_Vertices_of G) by A7, FUNCT_2:2;
reconsider t =
(the_Target_of G) +* f as
Function of
((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),
(the_Vertices_of G) by A8, A14, FUNCT_2:2;
set H =
createGraph (
(the_Vertices_of G),
((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),
s,
t);
A15:
(
the_Edges_of G c= the_Edges_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),s,t)) &
the_Vertices_of G = the_Vertices_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),s,t)) )
by XBOOLE_1:7;
now for e being set st e in the_Edges_of G holds
( (the_Source_of G) . e = (the_Source_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),s,t))) . e & (the_Target_of G) . e = (the_Target_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),s,t))) . e )let e be
set ;
( e in the_Edges_of G implies ( (the_Source_of G) . e = (the_Source_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),s,t))) . e & (the_Target_of G) . e = (the_Target_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),s,t))) . e ) )assume A16:
e in the_Edges_of G
;
( (the_Source_of G) . e = (the_Source_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),s,t))) . e & (the_Target_of G) . e = (the_Target_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),s,t))) . e )then
e in (the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V }
by XBOOLE_0:def 3;
then A17:
not
e in dom f
by A2, A9, A16, XBOOLE_0:5;
hence
(the_Source_of G) . e = (the_Source_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),s,t))) . e
by FUNCT_4:11;
(the_Target_of G) . e = (the_Target_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),s,t))) . ethus
(the_Target_of G) . e = (the_Target_of (createGraph ((the_Vertices_of G),((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),s,t))) . e
by A17, FUNCT_4:11;
verum end; then reconsider H =
createGraph (
(the_Vertices_of G),
((the_Edges_of G) \/ { [(the_Edges_of G),v] where v is Vertex of G : v in V } ),
s,
t) as
Supergraph of
G by A15, GLIB_006:def 9;
take H =
H;
( the_Vertices_of H = the_Vertices_of G & ex E being set ex f being one-to-one Function st
( E misses the_Edges_of G & the_Edges_of H = (the_Edges_of G) \/ E & dom f = E & rng f = V & the_Source_of H = (the_Source_of G) +* f & the_Target_of H = (the_Target_of G) +* f ) )thus
the_Vertices_of H = the_Vertices_of G
;
ex E being set ex f being one-to-one Function st
( E misses the_Edges_of G & the_Edges_of H = (the_Edges_of G) \/ E & dom f = E & rng f = V & the_Source_of H = (the_Source_of G) +* f & the_Target_of H = (the_Target_of G) +* f )now for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2let x1,
x2 be
object ;
( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )assume A19:
(
x1 in dom f &
x2 in dom f &
f . x1 = f . x2 )
;
x1 = x2then consider v1 being
Vertex of
G such that A20:
(
x1 = [(the_Edges_of G),v1] &
v1 in V )
by A2;
consider v2 being
Vertex of
G such that A21:
(
x2 = [(the_Edges_of G),v2] &
v2 in V )
by A2, A19;
thus x1 =
[(the_Edges_of G),([(the_Edges_of G),v1] `2)]
by A20
.=
[(the_Edges_of G),(f . x2)]
by A2, A19, A20
.=
[(the_Edges_of G),([(the_Edges_of G),v2] `2)]
by A2, A19, A21
.=
x2
by A21
;
verum end; then reconsider f =
f as
one-to-one Function by FUNCT_1:def 4;
take E =
{ [(the_Edges_of G),v] where v is Vertex of G : v in V } ;
ex f being one-to-one Function st
( E misses the_Edges_of G & the_Edges_of H = (the_Edges_of G) \/ E & dom f = E & rng f = V & the_Source_of H = (the_Source_of G) +* f & the_Target_of H = (the_Target_of G) +* f )take f =
f;
( E misses the_Edges_of G & the_Edges_of H = (the_Edges_of G) \/ E & dom f = E & rng f = V & the_Source_of H = (the_Source_of G) +* f & the_Target_of H = (the_Target_of G) +* f )thus
(
E misses the_Edges_of G &
the_Edges_of H = (the_Edges_of G) \/ E )
by A9;
( dom f = E & rng f = V & the_Source_of H = (the_Source_of G) +* f & the_Target_of H = (the_Target_of G) +* f )thus
(
dom f = E &
rng f = V )
by A2, A6;
( the_Source_of H = (the_Source_of G) +* f & the_Target_of H = (the_Target_of G) +* f )thus
(
the_Source_of H = (the_Source_of G) +* f &
the_Target_of H = (the_Target_of G) +* f )
;
verum
end;
assume
not V c= the_Vertices_of G
; ex b1 being Supergraph of G st b1 == G
take
G
; ( G is Supergraph of G & G == G )
thus
( G is Supergraph of G & G == G )
by GLIB_006:61; verum