let G3 be _Graph; :: thesis: for V1, V2 being Subset of (the_Vertices_of G3)
for G1 being addLoops of G3,V1 \/ V2 st V1 misses V2 holds
ex G2 being addLoops of G3,V1 st G1 is addLoops of G2,V2
let V1, V2 be Subset of (the_Vertices_of G3); :: thesis: for G1 being addLoops of G3,V1 \/ V2 st V1 misses V2 holds
ex G2 being addLoops of G3,V1 st G1 is addLoops of G2,V2
let G1 be addLoops of G3,V1 \/ V2; :: thesis: ( V1 misses V2 implies ex G2 being addLoops of G3,V1 st G1 is addLoops of G2,V2 )
assume A1: V1 misses V2 ; :: thesis: ex G2 being addLoops of G3,V1 st G1 is addLoops of G2,V2
consider E3 being set , f3 being one-to-one Function such that
A2: ( E3 misses the_Edges_of G3 & the_Edges_of G1 = (the_Edges_of G3) \/ E3 & dom f3 = E3 & rng f3 = V1 \/ V2 & the_Source_of G1 = (the_Source_of G3) +* f3 & the_Target_of G1 = (the_Target_of G3) +* f3 ) by Def5;
set E1 = f3 " V1;
set f1 = f3 | (f3 " V1);
set s1 = (the_Source_of G3) +* (f3 | (f3 " V1));
set t1 = (the_Target_of G3) +* (f3 | (f3 " V1));
A3: f3 " V1 c= E3 by A2, RELAT_1:132;
then A4: f3 " V1 = (f3 " V1) /\ E3 by XBOOLE_1:28
.= dom (f3 | (f3 " V1)) by A2, RELAT_1:61 ;
A5: dom ((the_Source_of G3) +* (f3 | (f3 " V1))) = (dom (the_Source_of G3)) \/ (dom (f3 | (f3 " V1))) by FUNCT_4:def 1
.= (the_Edges_of G3) \/ (f3 " V1) by A4, FUNCT_2:def 1 ;
A6: dom ((the_Target_of G3) +* (f3 | (f3 " V1))) = (dom (the_Target_of G3)) \/ (dom (f3 | (f3 " V1))) by FUNCT_4:def 1
.= (the_Edges_of G3) \/ (f3 " V1) by A4, FUNCT_2:def 1 ;
A7: V1 = f3 .: (f3 " V1) by A2, XBOOLE_1:7, FUNCT_1:77
.= rng (f3 | (f3 " V1)) by RELAT_1:115 ;
then A8: (the_Vertices_of G3) \/ (rng (f3 | (f3 " V1))) = the_Vertices_of G3 by XBOOLE_1:12;
A9: rng ((the_Source_of G3) +* (f3 | (f3 " V1))) c= (rng (the_Source_of G3)) \/ (rng (f3 | (f3 " V1))) by FUNCT_4:17;
(rng (the_Source_of G3)) \/ (rng (f3 | (f3 " V1))) c= (the_Vertices_of G3) \/ (rng (f3 | (f3 " V1))) by XBOOLE_1:9;
then reconsider s1 = (the_Source_of G3) +* (f3 | (f3 " V1)) as Function of ((the_Edges_of G3) \/ (f3 " V1)),(the_Vertices_of G3) by A5, A8, A9, XBOOLE_1:1, FUNCT_2:2;
A10: rng ((the_Target_of G3) +* (f3 | (f3 " V1))) c= (rng (the_Target_of G3)) \/ (rng (f3 | (f3 " V1))) by FUNCT_4:17;
(rng (the_Target_of G3)) \/ (rng (f3 | (f3 " V1))) c= (the_Vertices_of G3) \/ (rng (f3 | (f3 " V1))) by XBOOLE_1:9;
then reconsider t1 = (the_Target_of G3) +* (f3 | (f3 " V1)) as Function of ((the_Edges_of G3) \/ (f3 " V1)),(the_Vertices_of G3) by A6, A8, A10, XBOOLE_1:1, FUNCT_2:2;
set G2 = createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1);

now :: thesis: ( the_Vertices_of G3 c= the_Vertices_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1)) & the_Edges_of G3 c= the_Edges_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1)) & ( for e being set st e in the_Edges_of G3 holds
( (the_Source_of G3) . e = (the_Source_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1))) . e & (the_Target_of G3) . e = (the_Target_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1))) . e ) ) )

thus the_Vertices_of G3 c= the_Vertices_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1)) ; :: thesis: ( the_Edges_of G3 c= the_Edges_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1)) & ( for e being set st e in the_Edges_of G3 holds
( (the_Source_of G3) . e = (the_Source_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1))) . e & (the_Target_of G3) . e = (the_Target_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1))) . e ) ) )
thus the_Edges_of G3 c= the_Edges_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1)) by XBOOLE_1:7; :: thesis: for e being set st e in the_Edges_of G3 holds
( (the_Source_of G3) . e = (the_Source_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1))) . e & (the_Target_of G3) . e = (the_Target_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1))) . e )
let e be set ; :: thesis: ( e in the_Edges_of G3 implies ( (the_Source_of G3) . e = (the_Source_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1))) . e & (the_Target_of G3) . e = (the_Target_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1))) . e ) )
assume A11: e in the_Edges_of G3 ; :: thesis: ( (the_Source_of G3) . e = (the_Source_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1))) . e & (the_Target_of G3) . e = (the_Target_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1))) . e )
then e in (the_Edges_of G3) \/ E3 by XBOOLE_0:def 3;
then A12: not e in dom (f3 | (f3 " V1)) by A2, A3, A4, A11, XBOOLE_0:5;
thus (the_Source_of G3) . e = s1 . e by A12, FUNCT_4:11
.= (the_Source_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1))) . e ; :: thesis: (the_Target_of G3) . e = (the_Target_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1))) . e
thus (the_Target_of G3) . e = t1 . e by A12, FUNCT_4:11
.= (the_Target_of (createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1))) . e ; :: thesis: verum

end;

then reconsider G2 = createGraph ((the_Vertices_of G3),((the_Edges_of G3) \/ (f3 " V1)),s1,t1) as Supergraph of G3 by GLIB_006:def 9;

now :: thesis: ( the_Vertices_of G2 = the_Vertices_of G3 & ex E1 being set ex f1 being one-to-one Function st
( E1 misses the_Edges_of G3 & the_Edges_of G2 = (the_Edges_of G3) \/ E1 & dom f1 = E1 & rng f1 = V1 & the_Source_of G2 = (the_Source_of G3) +* f1 & the_Target_of G2 = (the_Target_of G3) +* f1 ) )

thus the_Vertices_of G2 = the_Vertices_of G3 ; :: thesis: ex E1 being set ex f1 being one-to-one Function st
( E1 misses the_Edges_of G3 & the_Edges_of G2 = (the_Edges_of G3) \/ E1 & dom f1 = E1 & rng f1 = V1 & the_Source_of G2 = (the_Source_of G3) +* f1 & the_Target_of G2 = (the_Target_of G3) +* f1 )
reconsider E1 = f3 " V1 as set ;
reconsider f1 = f3 | (f3 " V1) as one-to-one Function by FUNCT_1:52;
take E1 = E1; :: thesis: ex f1 being one-to-one Function st
( E1 misses the_Edges_of G3 & the_Edges_of G2 = (the_Edges_of G3) \/ E1 & dom f1 = E1 & rng f1 = V1 & the_Source_of G2 = (the_Source_of G3) +* f1 & the_Target_of G2 = (the_Target_of G3) +* f1 )
take f1 = f1; :: thesis: ( E1 misses the_Edges_of G3 & the_Edges_of G2 = (the_Edges_of G3) \/ E1 & dom f1 = E1 & rng f1 = V1 & the_Source_of G2 = (the_Source_of G3) +* f1 & the_Target_of G2 = (the_Target_of G3) +* f1 )
thus E1 misses the_Edges_of G3 by A2, A3, XBOOLE_1:63; :: thesis: ( the_Edges_of G2 = (the_Edges_of G3) \/ E1 & dom f1 = E1 & rng f1 = V1 & the_Source_of G2 = (the_Source_of G3) +* f1 & the_Target_of G2 = (the_Target_of G3) +* f1 )
thus the_Edges_of G2 = (the_Edges_of G3) \/ E1 ; :: thesis: ( dom f1 = E1 & rng f1 = V1 & the_Source_of G2 = (the_Source_of G3) +* f1 & the_Target_of G2 = (the_Target_of G3) +* f1 )
thus dom f1 = E1 by A4; :: thesis: ( rng f1 = V1 & the_Source_of G2 = (the_Source_of G3) +* f1 & the_Target_of G2 = (the_Target_of G3) +* f1 )
thus rng f1 = V1 by A7; :: thesis: ( the_Source_of G2 = (the_Source_of G3) +* f1 & the_Target_of G2 = (the_Target_of G3) +* f1 )
thus the_Source_of G2 = (the_Source_of G3) +* f1 ; :: thesis: the_Target_of G2 = (the_Target_of G3) +* f1
thus the_Target_of G2 = (the_Target_of G3) +* f1 ; :: thesis: verum

end;

then reconsider G2 = G2 as addLoops of G3,V1 by Def5;
take G2 ; :: thesis: G1 is addLoops of G2,V2
set E2 = E3 \ (f3 " V1);
A13: the_Vertices_of G1 = the_Vertices_of G3 by Def5
.= the_Vertices_of G2 ;
A14: the_Edges_of G1 = (the_Edges_of G3) \/ ((f3 " V1) \/ (E3 \ (f3 " V1))) by A2, A3, XBOOLE_1:45
.= ((the_Edges_of G3) \/ (f3 " V1)) \/ (E3 \ (f3 " V1)) by XBOOLE_1:4
.= (the_Edges_of G2) \/ (E3 \ (f3 " V1)) ;

now :: thesis: ( the_Vertices_of G2 c= the_Vertices_of G1 & the_Edges_of G2 c= the_Edges_of G1 & ( for e being set st e in the_Edges_of G2 holds
( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) ) )

thus the_Vertices_of G2 c= the_Vertices_of G1 by A13; :: thesis: ( the_Edges_of G2 c= the_Edges_of G1 & ( for e being set st e in the_Edges_of G2 holds
( (the_Source_of G2) . b₂ = (the_Source_of G1) . b₂ & (the_Target_of G2) . b₂ = (the_Target_of G1) . b₂ ) ) )
thus the_Edges_of G2 c= the_Edges_of G1 by A14, XBOOLE_1:7; :: thesis: for e being set st e in the_Edges_of G2 holds
( (the_Source_of G2) . b₂ = (the_Source_of G1) . b₂ & (the_Target_of G2) . b₂ = (the_Target_of G1) . b₂ )
let e be set ; :: thesis: ( e in the_Edges_of G2 implies ( (the_Source_of G2) . b₁ = (the_Source_of G1) . b₁ & (the_Target_of G2) . b₁ = (the_Target_of G1) . b₁ ) )
A15: f3 " V1 misses the_Edges_of G3 by A2, A3, XBOOLE_1:63;
assume e in the_Edges_of G2 ; :: thesis: ( (the_Source_of G2) . b₁ = (the_Source_of G1) . b₁ & (the_Target_of G2) . b₁ = (the_Target_of G1) . b₁ )
then A16: e in (the_Edges_of G3) \/ (f3 " V1) ;

per cases then ( e in the_Edges_of G3 or e in f3 " V1 ) by XBOOLE_0:def 3;

suppose A17: e in the_Edges_of G3 ; :: thesis: ( (the_Source_of G2) . b₁ = (the_Source_of G1) . b₁ & (the_Target_of G2) . b₁ = (the_Target_of G1) . b₁ )

then A18: not e in f3 " V1 by A15, A16, XBOOLE_0:5;
thus (the_Source_of G2) . e = s1 . e
.= (the_Source_of G3) . e by A4, A18, FUNCT_4:11
.= (the_Source_of G1) . e by A17, GLIB_006:def 9 ; :: thesis: (the_Target_of G2) . e = (the_Target_of G1) . e
thus (the_Target_of G2) . e = t1 . e
.= (the_Target_of G3) . e by A4, A18, FUNCT_4:11
.= (the_Target_of G1) . e by A17, GLIB_006:def 9 ; :: thesis: verum

end;

suppose A19: e in f3 " V1 ; :: thesis: ( (the_Source_of G2) . b₁ = (the_Source_of G1) . b₁ & (the_Target_of G2) . b₁ = (the_Target_of G1) . b₁ )

thus (the_Source_of G2) . e = s1 . e
.= (f3 | (f3 " V1)) . e by A4, A19, FUNCT_4:13
.= f3 . e by A19, FUNCT_1:49
.= (the_Source_of G1) . e by A2, A3, A19, FUNCT_4:13 ; :: thesis: (the_Target_of G2) . e = (the_Target_of G1) . e
thus (the_Target_of G2) . e = t1 . e
.= (f3 | (f3 " V1)) . e by A4, A19, FUNCT_4:13
.= f3 . e by A19, FUNCT_1:49
.= (the_Target_of G1) . e by A2, A3, A19, FUNCT_4:13 ; :: thesis: verum

end;

end;

end;

then A20: G1 is Supergraph of G2 by GLIB_006:def 9;

now :: thesis: ex E2 being set ex f2 being one-to-one Function st
( E2 misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E2 & dom f2 = E2 & rng f2 = V2 & the_Source_of G1 = (the_Source_of G2) +* f2 & the_Target_of G1 = (the_Target_of G2) +* f2 )

reconsider E2 = E3 \ (f3 " V1) as set ;
reconsider f2 = f3 | E2 as one-to-one Function by FUNCT_1:52;
take E2 = E2; :: thesis: ex f2 being one-to-one Function st
( E2 misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E2 & dom f2 = E2 & rng f2 = V2 & the_Source_of G1 = (the_Source_of G2) +* f2 & the_Target_of G1 = (the_Target_of G2) +* f2 )
take f2 = f2; :: thesis: ( E2 misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E2 & dom f2 = E2 & rng f2 = V2 & the_Source_of G1 = (the_Source_of G2) +* f2 & the_Target_of G1 = (the_Target_of G2) +* f2 )
E2 misses E3 \ E2 by XBOOLE_1:79;
then E2 misses E3 /\ (f3 " V1) by XBOOLE_1:48;
then A22: E2 misses f3 " V1 by A3, XBOOLE_1:28;
E2 misses the_Edges_of G3 by A2, XBOOLE_1:63;
then E2 misses (the_Edges_of G3) \/ (f3 " V1) by A22, XBOOLE_1:70;
hence E2 misses the_Edges_of G2 ; :: thesis: ( the_Edges_of G1 = (the_Edges_of G2) \/ E2 & dom f2 = E2 & rng f2 = V2 & the_Source_of G1 = (the_Source_of G2) +* f2 & the_Target_of G1 = (the_Target_of G2) +* f2 )
thus the_Edges_of G1 = (the_Edges_of G2) \/ E2 by A14; :: thesis: ( dom f2 = E2 & rng f2 = V2 & the_Source_of G1 = (the_Source_of G2) +* f2 & the_Target_of G1 = (the_Target_of G2) +* f2 )
A23: E2 = (f3 " (V1 \/ V2)) \ (f3 " V1) by A2, RELAT_1:134
.= f3 " ((V1 \/ V2) \ V1) by FUNCT_1:69
.= f3 " V2 by A1, XBOOLE_1:88 ;
thus dom f2 = (dom f3) /\ (f3 " V2) by A23, RELAT_1:61
.= E2 by A2, A23, XBOOLE_1:28 ; :: thesis: ( rng f2 = V2 & the_Source_of G1 = (the_Source_of G2) +* f2 & the_Target_of G1 = (the_Target_of G2) +* f2 )
thus rng f2 = f3 .: (f3 " V2) by A23, RELAT_1:115
.= V2 by A2, XBOOLE_1:7, FUNCT_1:77 ; :: thesis: ( the_Source_of G1 = (the_Source_of G2) +* f2 & the_Target_of G1 = (the_Target_of G2) +* f2 )
A24: dom f3 c= (f3 " V1) \/ E2 by A2, A3, XBOOLE_1:45;
thus the_Source_of G1 = (the_Source_of G3) +* ((f3 | (f3 " V1)) +* (f3 | E2)) by A2, A24, FUNCT_4:70
.= ((the_Source_of G3) +* (f3 | (f3 " V1))) +* f2 by FUNCT_4:14
.= (the_Source_of G2) +* f2 ; :: thesis: the_Target_of G1 = (the_Target_of G2) +* f2
thus the_Target_of G1 = (the_Target_of G3) +* ((f3 | (f3 " V1)) +* f2) by A2, A24, FUNCT_4:70
.= ((the_Target_of G3) +* (f3 | (f3 " V1))) +* f2 by FUNCT_4:14
.= (the_Target_of G2) +* f2 ; :: thesis: verum

end;

hence G1 is addLoops of G2,V2 by A13, A20, Def5; :: thesis: verum