let G3 be _Graph; for V1 being Subset of (the_Vertices_of G3)
for V2 being non empty Subset of (the_Vertices_of G3)
for G4 being inducedSubgraph of G3,V2
for G1 being addLoops of G3,V1
for G2 being inducedSubgraph of G1,V2 holds G2 is addLoops of G4,V1 /\ V2
let V1 be Subset of (the_Vertices_of G3); for V2 being non empty Subset of (the_Vertices_of G3)
for G4 being inducedSubgraph of G3,V2
for G1 being addLoops of G3,V1
for G2 being inducedSubgraph of G1,V2 holds G2 is addLoops of G4,V1 /\ V2
let V2 be non empty Subset of (the_Vertices_of G3); for G4 being inducedSubgraph of G3,V2
for G1 being addLoops of G3,V1
for G2 being inducedSubgraph of G1,V2 holds G2 is addLoops of G4,V1 /\ V2
let G4 be inducedSubgraph of G3,V2; for G1 being addLoops of G3,V1
for G2 being inducedSubgraph of G1,V2 holds G2 is addLoops of G4,V1 /\ V2
let G1 be addLoops of G3,V1; for G2 being inducedSubgraph of G1,V2 holds G2 is addLoops of G4,V1 /\ V2
let G2 be inducedSubgraph of G1,V2; G2 is addLoops of G4,V1 /\ V2
A1:
the_Vertices_of G1 = the_Vertices_of G3
by Def5;
A2:
the_Vertices_of G4 = V2
by GLIB_000:def 37;
A3:
the_Vertices_of G2 = V2
by A1, GLIB_000:def 37;
A4:
the_Edges_of G4 = G3 .edgesBetween V2
by GLIB_000:def 37;
A5:
the_Edges_of G2 = G1 .edgesBetween V2
by A1, GLIB_000:def 37;
consider E being set , f being one-to-one Function such that
A6:
( E misses the_Edges_of G3 & the_Edges_of G1 = (the_Edges_of G3) \/ E & dom f = E & rng f = V1 & the_Source_of G1 = (the_Source_of G3) +* f & the_Target_of G1 = (the_Target_of G3) +* f )
by Def5;
set g = f | (f " V2);
set D = dom (f | (f " V2));
then A14:
the_Edges_of G2 = (the_Edges_of G4) \/ (dom (f | (f " V2)))
by XBOOLE_0:def 3;
now ( the_Vertices_of G4 c= the_Vertices_of G2 & the_Edges_of G4 c= the_Edges_of G2 & ( for e being set st e in the_Edges_of G4 holds
( (the_Source_of G2) . e = (the_Source_of G4) . e & (the_Target_of G2) . e = (the_Target_of G4) . e ) ) )thus
the_Vertices_of G4 c= the_Vertices_of G2
by A2, A3;
( the_Edges_of G4 c= the_Edges_of G2 & ( for e being set st e in the_Edges_of G4 holds
( (the_Source_of G2) . e = (the_Source_of G4) . e & (the_Target_of G2) . e = (the_Target_of G4) . e ) ) )thus
the_Edges_of G4 c= the_Edges_of G2
by A14, XBOOLE_1:7;
for e being set st e in the_Edges_of G4 holds
( (the_Source_of G2) . e = (the_Source_of G4) . e & (the_Target_of G2) . e = (the_Target_of G4) . e )let e be
set ;
( e in the_Edges_of G4 implies ( (the_Source_of G2) . e = (the_Source_of G4) . e & (the_Target_of G2) . e = (the_Target_of G4) . e ) )set v =
(the_Source_of G4) . e;
set w =
(the_Target_of G4) . e;
assume A15:
e in the_Edges_of G4
;
( (the_Source_of G2) . e = (the_Source_of G4) . e & (the_Target_of G2) . e = (the_Target_of G4) . e )then
e DJoins (the_Source_of G4) . e,
(the_Target_of G4) . e,
G4
by GLIB_000:def 14;
then A16:
e DJoins (the_Source_of G4) . e,
(the_Target_of G4) . e,
G3
by GLIB_000:72;
then A17:
e DJoins (the_Source_of G4) . e,
(the_Target_of G4) . e,
G1
by GLIB_006:70;
then A18:
(
(the_Source_of G4) . e = (the_Source_of G1) . e &
(the_Target_of G4) . e = (the_Target_of G1) . e )
by GLIB_000:def 14;
(
(the_Source_of G4) . e = (the_Source_of G3) . e &
(the_Target_of G4) . e = (the_Target_of G3) . e )
by A16, GLIB_000:def 14;
then A19:
(
e in the_Edges_of G3 &
(the_Source_of G4) . e in V2 &
(the_Target_of G4) . e in V2 )
by A4, A15, GLIB_000:31;
the_Edges_of G3 c= the_Edges_of G1
by GLIB_006:def 9;
then
e in G1 .edgesBetween V2
by A19, A18, GLIB_000:31;
then
e DJoins (the_Source_of G4) . e,
(the_Target_of G4) . e,
G2
by A5, A17, GLIB_000:73;
hence
(
(the_Source_of G2) . e = (the_Source_of G4) . e &
(the_Target_of G2) . e = (the_Target_of G4) . e )
by GLIB_000:def 14;
verum end;
then A20:
G2 is Supergraph of G4
by GLIB_006:def 9;
A21:
V1 /\ V2 c= the_Vertices_of G4
by A2, XBOOLE_1:17;
now ( the_Vertices_of G2 = the_Vertices_of G4 & ex D being set ex g being one-to-one Function st
( D misses the_Edges_of G4 & the_Edges_of G2 = (the_Edges_of G4) \/ D & dom g = D & rng g = V1 /\ V2 & the_Source_of G2 = (the_Source_of G4) +* g & the_Target_of G2 = (the_Target_of G4) +* g ) )thus
the_Vertices_of G2 = the_Vertices_of G4
by A2, A3;
ex D being set ex g being one-to-one Function st
( D misses the_Edges_of G4 & the_Edges_of G2 = (the_Edges_of G4) \/ D & dom g = D & rng g = V1 /\ V2 & the_Source_of G2 = (the_Source_of G4) +* g & the_Target_of G2 = (the_Target_of G4) +* g )reconsider D =
dom (f | (f " V2)) as
set ;
reconsider g =
f | (f " V2) as
one-to-one Function by FUNCT_1:52;
take D =
D;
ex g being one-to-one Function st
( D misses the_Edges_of G4 & the_Edges_of G2 = (the_Edges_of G4) \/ D & dom g = D & rng g = V1 /\ V2 & the_Source_of G2 = (the_Source_of G4) +* g & the_Target_of G2 = (the_Target_of G4) +* g )take g =
g;
( D misses the_Edges_of G4 & the_Edges_of G2 = (the_Edges_of G4) \/ D & dom g = D & rng g = V1 /\ V2 & the_Source_of G2 = (the_Source_of G4) +* g & the_Target_of G2 = (the_Target_of G4) +* g )
(
D c= dom f &
the_Edges_of G4 c= the_Edges_of G3 )
by RELAT_1:60;
hence A22:
D misses the_Edges_of G4
by A6, XBOOLE_1:64;
( the_Edges_of G2 = (the_Edges_of G4) \/ D & dom g = D & rng g = V1 /\ V2 & the_Source_of G2 = (the_Source_of G4) +* g & the_Target_of G2 = (the_Target_of G4) +* g )thus
the_Edges_of G2 = (the_Edges_of G4) \/ D
by A14;
( dom g = D & rng g = V1 /\ V2 & the_Source_of G2 = (the_Source_of G4) +* g & the_Target_of G2 = (the_Target_of G4) +* g )thus
dom g = D
;
( rng g = V1 /\ V2 & the_Source_of G2 = (the_Source_of G4) +* g & the_Target_of G2 = (the_Target_of G4) +* g )thus rng g =
f .: (f " V2)
by RELAT_1:115
.=
V2 /\ (f .: (dom f))
by FUNCT_1:78
.=
V1 /\ V2
by A6, RELAT_1:113
;
( the_Source_of G2 = (the_Source_of G4) +* g & the_Target_of G2 = (the_Target_of G4) +* g )A23:
dom (the_Source_of G2) =
(the_Edges_of G4) \/ D
by A14, FUNCT_2:def 1
.=
(dom (the_Source_of G4)) \/ (dom g)
by FUNCT_2:def 1
.=
dom ((the_Source_of G4) +* g)
by FUNCT_4:def 1
;
now for x being object st x in dom (the_Source_of G2) holds
(the_Source_of G2) . x = ((the_Source_of G4) +* g) . xlet x be
object ;
( x in dom (the_Source_of G2) implies (the_Source_of G2) . b1 = ((the_Source_of G4) +* g) . b1 )assume
x in dom (the_Source_of G2)
;
(the_Source_of G2) . b1 = ((the_Source_of G4) +* g) . b1then A24:
x in (the_Edges_of G4) \/ D
by A14;
per cases then
( x in the_Edges_of G4 or x in D )
by XBOOLE_0:def 3;
suppose A27:
x in D
;
(the_Source_of G2) . b1 = ((the_Source_of G4) +* g) . b1then A28:
x in f " V2
by RELAT_1:57;
then A29:
(
x in dom f &
f . x in V2 )
by FUNCT_1:def 7;
then A30:
(
(the_Source_of G1) . x = f . x &
(the_Target_of G1) . x = f . x )
by A6, FUNCT_4:13;
x in the_Edges_of G1
by A6, A29, XBOOLE_0:def 3;
then A31:
x Joins f . x,
f . x,
G1
by A30, GLIB_000:def 13;
then
x in G1 .edgesBetween V2
by A29, GLIB_000:32;
then
x Joins f . x,
f . x,
G2
by A5, A31, GLIB_000:73;
hence (the_Source_of G2) . x =
f . x
by GLIB_000:def 13
.=
g . x
by A28, FUNCT_1:49
.=
((the_Source_of G4) +* g) . x
by A27, FUNCT_4:13
;
verum end; end; end; hence
the_Source_of G2 = (the_Source_of G4) +* g
by A23, FUNCT_1:2;
the_Target_of G2 = (the_Target_of G4) +* gA32:
dom (the_Target_of G2) =
(the_Edges_of G4) \/ D
by A14, FUNCT_2:def 1
.=
(dom (the_Target_of G4)) \/ (dom g)
by FUNCT_2:def 1
.=
dom ((the_Target_of G4) +* g)
by FUNCT_4:def 1
;
now for x being object st x in dom (the_Target_of G2) holds
(the_Target_of G2) . x = ((the_Target_of G4) +* g) . xlet x be
object ;
( x in dom (the_Target_of G2) implies (the_Target_of G2) . b1 = ((the_Target_of G4) +* g) . b1 )assume
x in dom (the_Target_of G2)
;
(the_Target_of G2) . b1 = ((the_Target_of G4) +* g) . b1then A33:
x in (the_Edges_of G4) \/ D
by A14;
per cases then
( x in the_Edges_of G4 or x in D )
by XBOOLE_0:def 3;
suppose A36:
x in D
;
(the_Target_of G2) . b1 = ((the_Target_of G4) +* g) . b1then A37:
x in f " V2
by RELAT_1:57;
then A38:
(
x in dom f &
f . x in V2 )
by FUNCT_1:def 7;
then A39:
(
(the_Source_of G1) . x = f . x &
(the_Target_of G1) . x = f . x )
by A6, FUNCT_4:13;
x in the_Edges_of G1
by A6, A38, XBOOLE_0:def 3;
then A40:
x Joins f . x,
f . x,
G1
by A39, GLIB_000:def 13;
then
x in G1 .edgesBetween V2
by A38, GLIB_000:32;
then
x Joins f . x,
f . x,
G2
by A5, A40, GLIB_000:73;
hence (the_Target_of G2) . x =
f . x
by GLIB_000:def 13
.=
g . x
by A37, FUNCT_1:49
.=
((the_Target_of G4) +* g) . x
by A36, FUNCT_4:13
;
verum end; end; end; hence
the_Target_of G2 = (the_Target_of G4) +* g
by A32, FUNCT_1:2;
verum end;
hence
G2 is addLoops of G4,V1 /\ V2
by A20, A21, Def5; verum