let G2 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V holds
( G1 .supDegree() = G2 .supDegree() & G1 .supInDegree() = G2 .supInDegree() & G1 .supOutDegree() = G2 .supOutDegree() )
let V be set ; :: thesis: for G1 being addVertices of G2,V holds
( G1 .supDegree() = G2 .supDegree() & G1 .supInDegree() = G2 .supInDegree() & G1 .supOutDegree() = G2 .supOutDegree() )
let G1 be addVertices of G2,V; :: thesis: ( G1 .supDegree() = G2 .supDegree() & G1 .supInDegree() = G2 .supInDegree() & G1 .supOutDegree() = G2 .supOutDegree() )
G2 is Subgraph of G1 by GLIB_006:57;
then A1: ( G2 .supDegree() c= G1 .supDegree() & G2 .supInDegree() c= G1 .supInDegree() & G2 .supOutDegree() c= G1 .supOutDegree() ) by Th63;
A2: the_Vertices_of G1 = (the_Vertices_of G2) \/ V by GLIB_006:def 10;
set D1 = { (v .degree()) where v is Vertex of G1 : verum } ;
set D2 = { (v .degree()) where v is Vertex of G2 : verum } ;
now :: thesis: for x being object st x in G1 .supDegree() holds
x in G2 .supDegree()
let x be object ; :: thesis: ( x in G1 .supDegree() implies x in G2 .supDegree() )
assume x in G1 .supDegree() ; :: thesis: x in G2 .supDegree()
then consider d1 being set such that
A3: ( x in d1 & d1 in { (v .degree()) where v is Vertex of G1 : verum } ) by TARSKI:def 4;
consider v1 being Vertex of G1 such that
A4: d1 = v1 .degree() by A3;
not v1 in V \ (the_Vertices_of G2) by A3, A4, GLIBPRE0:35, GLIB_006:88;
then ( v1 in the_Vertices_of G2 or not v1 in V ) by XBOOLE_0:def 5;
then reconsider v2 = v1 as Vertex of G2 by A2, XBOOLE_0:def 3;
( d1 = v2 .degree() & v2 .degree() in { (v .degree()) where v is Vertex of G2 : verum } ) by A4, GLIBPRE0:47;
hence x in G2 .supDegree() by A3, TARSKI:def 4; :: thesis: verum
end;
then G1 .supDegree() c= G2 .supDegree() by TARSKI:def 3;
hence G1 .supDegree() = G2 .supDegree() by A1, XBOOLE_0:def 10; :: thesis: ( G1 .supInDegree() = G2 .supInDegree() & G1 .supOutDegree() = G2 .supOutDegree() )
set D3 = { (v .inDegree()) where v is Vertex of G1 : verum } ;
set D4 = { (v .inDegree()) where v is Vertex of G2 : verum } ;
now :: thesis: for x being object st x in G1 .supInDegree() holds
x in G2 .supInDegree()
let x be object ; :: thesis: ( x in G1 .supInDegree() implies x in G2 .supInDegree() )
assume x in G1 .supInDegree() ; :: thesis: x in G2 .supInDegree()
then consider d1 being set such that
A5: ( x in d1 & d1 in { (v .inDegree()) where v is Vertex of G1 : verum } ) by TARSKI:def 4;
consider v1 being Vertex of G1 such that
A6: d1 = v1 .inDegree() by A5;
not v1 is isolated by A5, A6, GLIBPRE0:34;
then not v1 in V \ (the_Vertices_of G2) by GLIB_006:88;
then ( v1 in the_Vertices_of G2 or not v1 in V ) by XBOOLE_0:def 5;
then reconsider v2 = v1 as Vertex of G2 by A2, XBOOLE_0:def 3;
( d1 = v2 .inDegree() & v2 .inDegree() in { (v .inDegree()) where v is Vertex of G2 : verum } ) by A6, GLIBPRE0:47;
hence x in G2 .supInDegree() by A5, TARSKI:def 4; :: thesis: verum
end;
then G1 .supInDegree() c= G2 .supInDegree() by TARSKI:def 3;
hence G1 .supInDegree() = G2 .supInDegree() by A1, XBOOLE_0:def 10; :: thesis: G1 .supOutDegree() = G2 .supOutDegree()
set D5 = { (v .outDegree()) where v is Vertex of G1 : verum } ;
set D6 = { (v .outDegree()) where v is Vertex of G2 : verum } ;
now :: thesis: for x being object st x in G1 .supOutDegree() holds
x in G2 .supOutDegree()
let x be object ; :: thesis: ( x in G1 .supOutDegree() implies x in G2 .supOutDegree() )
assume x in G1 .supOutDegree() ; :: thesis: x in G2 .supOutDegree()
then consider d1 being set such that
A7: ( x in d1 & d1 in { (v .outDegree()) where v is Vertex of G1 : verum } ) by TARSKI:def 4;
consider v1 being Vertex of G1 such that
A8: d1 = v1 .outDegree() by A7;
not v1 is isolated by A7, A8, GLIBPRE0:34;
then not v1 in V \ (the_Vertices_of G2) by GLIB_006:88;
then ( v1 in the_Vertices_of G2 or not v1 in V ) by XBOOLE_0:def 5;
then reconsider v2 = v1 as Vertex of G2 by A2, XBOOLE_0:def 3;
( d1 = v2 .outDegree() & v2 .outDegree() in { (v .outDegree()) where v is Vertex of G2 : verum } ) by A8, GLIBPRE0:47;
hence x in G2 .supOutDegree() by A7, TARSKI:def 4; :: thesis: verum
end;
then G1 .supOutDegree() c= G2 .supOutDegree() by TARSKI:def 3;
hence G1 .supOutDegree() = G2 .supOutDegree() by A1, XBOOLE_0:def 10; :: thesis: verum