let G be _Graph; :: thesis: for V1, V2 being Subset of (the_Vertices_of G)
for G1 being addLoops of G,V1
for G2 being addLoops of G1,V2 st V1 misses V2 holds
G2 is addLoops of G,V1 \/ V2
let V1, V2 be Subset of (the_Vertices_of G); :: thesis: for G1 being addLoops of G,V1
for G2 being addLoops of G1,V2 st V1 misses V2 holds
G2 is addLoops of G,V1 \/ V2
let G1 be addLoops of G,V1; :: thesis: for G2 being addLoops of G1,V2 st V1 misses V2 holds
G2 is addLoops of G,V1 \/ V2
let G2 be addLoops of G1,V2; :: thesis: ( V1 misses V2 implies G2 is addLoops of G,V1 \/ V2 )
assume A1: V1 misses V2 ; :: thesis: G2 is addLoops of G,V1 \/ V2
consider E1 being set , f1 being one-to-one Function such that
A2: ( E1 misses the_Edges_of G & the_Edges_of G1 = (the_Edges_of G) \/ E1 & dom f1 = E1 & rng f1 = V1 & the_Source_of G1 = (the_Source_of G) +* f1 & the_Target_of G1 = (the_Target_of G) +* f1 ) by Def5;
V2 c= the_Vertices_of G ;
then V2 c= the_Vertices_of G1 by Th15;
then consider E2 being set , f2 being one-to-one Function such that
A3: ( E2 misses the_Edges_of G1 & the_Edges_of G2 = (the_Edges_of G1) \/ E2 & dom f2 = E2 & rng f2 = V2 & the_Source_of G2 = (the_Source_of G1) +* f2 & the_Target_of G2 = (the_Target_of G1) +* f2 ) by Def5;
A4: G2 is Supergraph of G by GLIB_006:62;
A5: the_Vertices_of G2 = the_Vertices_of G1 by Th15
.= the_Vertices_of G by Th15 ;

now :: thesis: ex E being set ex f being one-to-one Function st
( E misses the_Edges_of G & the_Edges_of G2 = (the_Edges_of G) \/ E & dom f = E & rng f = V1 \/ V2 & the_Source_of G2 = (the_Source_of G) +* f & the_Target_of G2 = (the_Target_of G) +* f )

reconsider E = E1 \/ E2 as set ;
reconsider f = f1 +* f2 as one-to-one Function by A1, A2, A3, FUNCT_4:92;
take E = E; :: thesis: ex f being one-to-one Function st
( E misses the_Edges_of G & the_Edges_of G2 = (the_Edges_of G) \/ E & dom f = E & rng f = V1 \/ V2 & the_Source_of G2 = (the_Source_of G) +* f & the_Target_of G2 = (the_Target_of G) +* f )
take f = f; :: thesis: ( E misses the_Edges_of G & the_Edges_of G2 = (the_Edges_of G) \/ E & dom f = E & rng f = V1 \/ V2 & the_Source_of G2 = (the_Source_of G) +* f & the_Target_of G2 = (the_Target_of G) +* f )
A6: ( E2 misses the_Edges_of G & E2 misses E1 ) by A2, A3, XBOOLE_1:70;
hence E misses the_Edges_of G by A2, XBOOLE_1:70; :: thesis: ( the_Edges_of G2 = (the_Edges_of G) \/ E & dom f = E & rng f = V1 \/ V2 & the_Source_of G2 = (the_Source_of G) +* f & the_Target_of G2 = (the_Target_of G) +* f )
thus the_Edges_of G2 = (the_Edges_of G) \/ E by A2, A3, XBOOLE_1:4; :: thesis: ( dom f = E & rng f = V1 \/ V2 & the_Source_of G2 = (the_Source_of G) +* f & the_Target_of G2 = (the_Target_of G) +* f )
thus dom f = E by A2, A3, FUNCT_4:def 1; :: thesis: ( rng f = V1 \/ V2 & the_Source_of G2 = (the_Source_of G) +* f & the_Target_of G2 = (the_Target_of G) +* f )
thus rng f = V1 \/ V2 by A2, A3, A6, NECKLACE:6; :: thesis: ( the_Source_of G2 = (the_Source_of G) +* f & the_Target_of G2 = (the_Target_of G) +* f )
thus the_Source_of G2 = (the_Source_of G) +* f by A2, A3, FUNCT_4:14; :: thesis: the_Target_of G2 = (the_Target_of G) +* f
thus the_Target_of G2 = (the_Target_of G) +* f by A2, A3, FUNCT_4:14; :: thesis: verum

end;

hence G2 is addLoops of G,V1 \/ V2 by A4, A5, Def5; :: thesis: verum