let G3 be _Graph; :: thesis: 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); :: thesis: 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); :: thesis: 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; :: thesis: 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; :: thesis: for G2 being inducedSubgraph of G1,V2 holds G2 is addLoops of G4,V1 /\ V2
let G2 be inducedSubgraph of G1,V2; :: thesis: 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));

now :: thesis: for e being object holds
( ( not e in the_Edges_of G2 or e in the_Edges_of G4 or e in dom (f | (f " V2)) ) & ( ( e in the_Edges_of G4 or e in dom (f | (f " V2)) ) implies e in the_Edges_of G2 ) )

let e be object ; :: thesis: ( ( not e in the_Edges_of G2 or e in the_Edges_of G4 or e in dom (f | (f " V2)) ) & ( ( e in the_Edges_of G4 or e in dom (f | (f " V2)) ) implies b₁ in the_Edges_of G2 ) )
thus ( not e in the_Edges_of G2 or e in the_Edges_of G4 or e in dom (f | (f " V2)) ) :: thesis: ( ( e in the_Edges_of G4 or e in dom (f | (f " V2)) ) implies b₁ in the_Edges_of G2 )

proof

assume e in the_Edges_of G2 ; :: thesis: ( e in the_Edges_of G4 or e in dom (f | (f " V2)) )
then A7: ( e in the_Edges_of G1 & (the_Source_of G1) . e in V2 & (the_Target_of G1) . e in V2 ) by A5, GLIB_000:31;

per cases then ( e in the_Edges_of G3 or e in E ) by A6, XBOOLE_0:def 3;

suppose A8: e in the_Edges_of G3 ; :: thesis: ( e in the_Edges_of G4 or e in dom (f | (f " V2)) )

then ( (the_Source_of G3) . e in V2 & (the_Target_of G3) . e in V2 ) by A7, GLIB_006:def 9;
hence ( e in the_Edges_of G4 or e in dom (f | (f " V2)) ) by A4, A8, GLIB_000:31; :: thesis: verum

end;

suppose A9: e in E ; :: thesis: ( e in the_Edges_of G4 or e in dom (f | (f " V2)) )

then (the_Source_of G1) . e = f . e by A6, FUNCT_4:13;
then e in f " V2 by A6, A7, A9, FUNCT_1:def 7;
hence ( e in the_Edges_of G4 or e in dom (f | (f " V2)) ) by A6, A9, RELAT_1:57; :: thesis: verum

end;

end;

end;

assume ( e in the_Edges_of G4 or e in dom (f | (f " V2)) ) ; :: thesis: b₁ in the_Edges_of G2

per cases then ( e in the_Edges_of G4 or e in dom (f | (f " V2)) ) ;

suppose e in the_Edges_of G4 ; :: thesis: b₁ in the_Edges_of G2

then A10: ( e in the_Edges_of G3 & (the_Source_of G3) . e in V2 & (the_Target_of G3) . e in V2 ) by A4, GLIB_000:31;
then A11: ( (the_Source_of G3) . e = (the_Source_of G1) . e & (the_Target_of G3) . e = (the_Target_of G1) . e ) by GLIB_006:def 9;
the_Edges_of G3 c= the_Edges_of G1 by GLIB_006:def 9;
hence e in the_Edges_of G2 by A5, A10, A11, GLIB_000:31; :: thesis: verum

end;

suppose e in dom (f | (f " V2)) ; :: thesis: b₁ in the_Edges_of G2

then e in f " V2 by RELAT_1:57;
then A12: ( e in dom f & f . e in V2 ) by FUNCT_1:def 7;
then A13: ( (the_Source_of G1) . e in V2 & (the_Target_of G1) . e in V2 ) by A6, FUNCT_4:13;
e in the_Edges_of G1 by A6, A12, XBOOLE_0:def 3;
hence e in the_Edges_of G2 by A5, A13, GLIB_000:31; :: thesis: verum

end;

end;

end;

then A14: the_Edges_of G2 = (the_Edges_of G4) \/ (dom (f | (f " V2))) by XBOOLE_0:def 3;

now :: thesis: ( 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; :: thesis: ( 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( (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; :: thesis: 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 :: thesis: ( 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 :: thesis: for x being object st x in dom (the_Source_of G2) holds
(the_Source_of G2) . x = ((the_Source_of G4) +* g) . x

let x be object ; :: thesis: ( x in dom (the_Source_of G2) implies (the_Source_of G2) . b₁ = ((the_Source_of G4) +* g) . b₁ )
assume x in dom (the_Source_of G2) ; :: thesis: (the_Source_of G2) . b₁ = ((the_Source_of G4) +* g) . b₁
then 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 A25: x in the_Edges_of G4 ; :: thesis: (the_Source_of G2) . b₁ = ((the_Source_of G4) +* g) . b₁

then A26: not x in D by A22, A24, XBOOLE_0:5;
thus (the_Source_of G2) . x = (the_Source_of G4) . x by A20, A25, GLIB_006:def 9
.= ((the_Source_of G4) +* g) . x by A26, FUNCT_4:11 ; :: thesis: verum

end;

suppose A27: x in D ; :: thesis: (the_Source_of G2) . b₁ = ((the_Source_of G4) +* g) . b₁

then 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 ;
:: thesis: verum

end;

end;

end;

hence the_Source_of G2 = (the_Source_of G4) +* g by A23, FUNCT_1:2; :: thesis: the_Target_of G2 = (the_Target_of G4) +* g
A32: 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 :: thesis: for x being object st x in dom (the_Target_of G2) holds
(the_Target_of G2) . x = ((the_Target_of G4) +* g) . x

let x be object ; :: thesis: ( x in dom (the_Target_of G2) implies (the_Target_of G2) . b₁ = ((the_Target_of G4) +* g) . b₁ )
assume x in dom (the_Target_of G2) ; :: thesis: (the_Target_of G2) . b₁ = ((the_Target_of G4) +* g) . b₁
then 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 A34: x in the_Edges_of G4 ; :: thesis: (the_Target_of G2) . b₁ = ((the_Target_of G4) +* g) . b₁

then A35: not x in D by A22, A33, XBOOLE_0:5;
thus (the_Target_of G2) . x = (the_Target_of G4) . x by A20, A34, GLIB_006:def 9
.= ((the_Target_of G4) +* g) . x by A35, FUNCT_4:11 ; :: thesis: verum

end;

suppose A36: x in D ; :: thesis: (the_Target_of G2) . b₁ = ((the_Target_of G4) +* g) . b₁

then 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 ;
:: thesis: verum

end;

end;

end;

hence the_Target_of G2 = (the_Target_of G4) +* g by A32, FUNCT_1:2; :: thesis: verum

end;

hence G2 is addLoops of G4,V1 /\ V2 by A20, A21, Def5; :: thesis: verum