let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies ( G1 .supDegree() = G2 .supDegree() & G1 .minDegree() = G2 .minDegree() & G1 .supInDegree() = G2 .supInDegree() & G1 .minInDegree() = G2 .minInDegree() & G1 .supOutDegree() = G2 .supOutDegree() & G1 .minOutDegree() = G2 .minOutDegree() ) )
assume A1: G1 == G2 ; :: thesis: ( G1 .supDegree() = G2 .supDegree() & G1 .minDegree() = G2 .minDegree() & G1 .supInDegree() = G2 .supInDegree() & G1 .minInDegree() = G2 .minInDegree() & G1 .supOutDegree() = G2 .supOutDegree() & G1 .minOutDegree() = G2 .minOutDegree() )
set S1 = { (v .degree()) where v is Vertex of G1 : verum } ;
set S2 = { (v .degree()) where v is Vertex of G2 : verum } ;
now :: thesis: for x being object holds
( ( x in { (v .degree()) where v is Vertex of G1 : verum } implies x in { (v .degree()) where v is Vertex of G2 : verum } ) & ( x in { (v .degree()) where v is Vertex of G2 : verum } implies x in { (v .degree()) where v is Vertex of G1 : verum } ) )
let x be object ; :: thesis: ( ( x in { (v .degree()) where v is Vertex of G1 : verum } implies x in { (v .degree()) where v is Vertex of G2 : verum } ) & ( x in { (v .degree()) where v is Vertex of G2 : verum } implies x in { (v .degree()) where v is Vertex of G1 : verum } ) )
hereby :: thesis: ( x in { (v .degree()) where v is Vertex of G2 : verum } implies x in { (v .degree()) where v is Vertex of G1 : verum } )
assume x in { (v .degree()) where v is Vertex of G1 : verum } ; :: thesis: x in { (v .degree()) where v is Vertex of G2 : verum }
then consider v1 being Vertex of G1 such that
A2: x = v1 .degree() ;
reconsider v2 = v1 as Vertex of G2 by A1, GLIB_000:def 34;
x = v2 .degree() by A1, A2, GLIB_000:96;
hence x in { (v .degree()) where v is Vertex of G2 : verum } ; :: thesis: verum
end;
assume x in { (v .degree()) where v is Vertex of G2 : verum } ; :: thesis: x in { (v .degree()) where v is Vertex of G1 : verum }
then consider v2 being Vertex of G2 such that
A3: x = v2 .degree() ;
reconsider v1 = v2 as Vertex of G1 by A1, GLIB_000:def 34;
x = v1 .degree() by A1, A3, GLIB_000:96;
hence x in { (v .degree()) where v is Vertex of G1 : verum } ; :: thesis: verum
end;
hence ( G1 .supDegree() = G2 .supDegree() & G1 .minDegree() = G2 .minDegree() ) by TARSKI:2; :: thesis: ( G1 .supInDegree() = G2 .supInDegree() & G1 .minInDegree() = G2 .minInDegree() & G1 .supOutDegree() = G2 .supOutDegree() & G1 .minOutDegree() = G2 .minOutDegree() )
set S3 = { (v .inDegree()) where v is Vertex of G1 : verum } ;
set S4 = { (v .inDegree()) where v is Vertex of G2 : verum } ;
now :: thesis: for x being object holds
( ( x in { (v .inDegree()) where v is Vertex of G1 : verum } implies x in { (v .inDegree()) where v is Vertex of G2 : verum } ) & ( x in { (v .inDegree()) where v is Vertex of G2 : verum } implies x in { (v .inDegree()) where v is Vertex of G1 : verum } ) )
let x be object ; :: thesis: ( ( x in { (v .inDegree()) where v is Vertex of G1 : verum } implies x in { (v .inDegree()) where v is Vertex of G2 : verum } ) & ( x in { (v .inDegree()) where v is Vertex of G2 : verum } implies x in { (v .inDegree()) where v is Vertex of G1 : verum } ) )
hereby :: thesis: ( x in { (v .inDegree()) where v is Vertex of G2 : verum } implies x in { (v .inDegree()) where v is Vertex of G1 : verum } )
assume x in { (v .inDegree()) where v is Vertex of G1 : verum } ; :: thesis: x in { (v .inDegree()) where v is Vertex of G2 : verum }
then consider v1 being Vertex of G1 such that
A4: x = v1 .inDegree() ;
reconsider v2 = v1 as Vertex of G2 by A1, GLIB_000:def 34;
x = v2 .inDegree() by A1, A4, GLIB_000:96;
hence x in { (v .inDegree()) where v is Vertex of G2 : verum } ; :: thesis: verum
end;
assume x in { (v .inDegree()) where v is Vertex of G2 : verum } ; :: thesis: x in { (v .inDegree()) where v is Vertex of G1 : verum }
then consider v2 being Vertex of G2 such that
A5: x = v2 .inDegree() ;
reconsider v1 = v2 as Vertex of G1 by A1, GLIB_000:def 34;
x = v1 .inDegree() by A1, A5, GLIB_000:96;
hence x in { (v .inDegree()) where v is Vertex of G1 : verum } ; :: thesis: verum
end;
hence ( G1 .supInDegree() = G2 .supInDegree() & G1 .minInDegree() = G2 .minInDegree() ) by TARSKI:2; :: thesis: ( G1 .supOutDegree() = G2 .supOutDegree() & G1 .minOutDegree() = G2 .minOutDegree() )
set S5 = { (v .outDegree()) where v is Vertex of G1 : verum } ;
set S6 = { (v .outDegree()) where v is Vertex of G2 : verum } ;
now :: thesis: for x being object holds
( ( x in { (v .outDegree()) where v is Vertex of G1 : verum } implies x in { (v .outDegree()) where v is Vertex of G2 : verum } ) & ( x in { (v .outDegree()) where v is Vertex of G2 : verum } implies x in { (v .outDegree()) where v is Vertex of G1 : verum } ) )
let x be object ; :: thesis: ( ( x in { (v .outDegree()) where v is Vertex of G1 : verum } implies x in { (v .outDegree()) where v is Vertex of G2 : verum } ) & ( x in { (v .outDegree()) where v is Vertex of G2 : verum } implies x in { (v .outDegree()) where v is Vertex of G1 : verum } ) )
hereby :: thesis: ( x in { (v .outDegree()) where v is Vertex of G2 : verum } implies x in { (v .outDegree()) where v is Vertex of G1 : verum } )
assume x in { (v .outDegree()) where v is Vertex of G1 : verum } ; :: thesis: x in { (v .outDegree()) where v is Vertex of G2 : verum }
then consider v1 being Vertex of G1 such that
A6: x = v1 .outDegree() ;
reconsider v2 = v1 as Vertex of G2 by A1, GLIB_000:def 34;
x = v2 .outDegree() by A1, A6, GLIB_000:96;
hence x in { (v .outDegree()) where v is Vertex of G2 : verum } ; :: thesis: verum
end;
assume x in { (v .outDegree()) where v is Vertex of G2 : verum } ; :: thesis: x in { (v .outDegree()) where v is Vertex of G1 : verum }
then consider v2 being Vertex of G2 such that
A7: x = v2 .outDegree() ;
reconsider v1 = v2 as Vertex of G1 by A1, GLIB_000:def 34;
x = v1 .outDegree() by A1, A7, GLIB_000:96;
hence x in { (v .outDegree()) where v is Vertex of G1 : verum } ; :: thesis: verum
end;
hence ( G1 .supOutDegree() = G2 .supOutDegree() & G1 .minOutDegree() = G2 .minOutDegree() ) by TARSKI:2; :: thesis: verum