let G2 be _Graph; for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & not v1 in V holds
( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
let V be Subset of (the_Vertices_of G2); for G1 being addLoops of G2,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & not v1 in V holds
( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
let G1 be addLoops of G2,V; for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & not v1 in V holds
( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
let v1 be Vertex of G1; for v2 being Vertex of G2 st v1 = v2 & not v1 in V holds
( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
let v2 be Vertex of G2; ( v1 = v2 & not v1 in V implies ( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() ) )
assume A1:
( v1 = v2 & not v1 in V )
; ( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
consider E being set , f being one-to-one Function such that
A2:
( E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E )
and
A3:
( dom f = E & rng f = V & the_Source_of G1 = (the_Source_of G2) +* f )
and
A4:
the_Target_of G1 = (the_Target_of G2) +* f
by Def5;
A5:
G2 is Subgraph of G1
by GLIB_006:57;
then A6:
v2 .edgesIn() c= v1 .edgesIn()
by A1, GLIB_000:78;
now for e being object st e in v1 .edgesIn() holds
e in v2 .edgesIn() let e be
object ;
( e in v1 .edgesIn() implies e in v2 .edgesIn() )assume
e in v1 .edgesIn()
;
e in v2 .edgesIn() then consider x being
set such that A7:
e DJoins x,
v1,
G1
by GLIB_000:57;
e in the_Edges_of G2
proof
assume A8:
not
e in the_Edges_of G2
;
contradiction
e in the_Edges_of G1
by A7, GLIB_000:def 14;
then A9:
e in E
by A2, A8, XBOOLE_0:def 3;
v1 =
(the_Target_of G1) . e
by A7, GLIB_000:def 14
.=
f . e
by A3, A4, A9, FUNCT_4:13
;
hence
contradiction
by A1, A3, A9, FUNCT_1:3;
verum
end; hence
e in v2 .edgesIn()
by A1, A7, GLIB_006:71, GLIB_000:57;
verum end;
then
v1 .edgesIn() c= v2 .edgesIn()
by TARSKI:def 3;
hence A10:
v1 .edgesIn() = v2 .edgesIn()
by A6, XBOOLE_0:def 10; ( v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
hence
v1 .inDegree() = v2 .inDegree()
; ( v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
A11:
v2 .edgesOut() c= v1 .edgesOut()
by A1, A5, GLIB_000:78;
then
v1 .edgesOut() c= v2 .edgesOut()
by TARSKI:def 3;
hence A15:
v1 .edgesOut() = v2 .edgesOut()
by A11, XBOOLE_0:def 10; ( v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
hence
v1 .outDegree() = v2 .outDegree()
; ( v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
thus
( v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
by A10, A15; verum