let G2 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V
for x, y being set
for e being object holds
( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
let V be set ; :: thesis: for G1 being addVertices of G2,V
for x, y being set
for e being object holds
( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
let G1 be addVertices of G2,V; :: thesis: for x, y being set
for e being object holds
( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
let x, y be set ; :: thesis: for e being object holds
( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
let e be object ; :: thesis: ( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
set v1 = (the_Source_of G1) . e;
set w1 = (the_Target_of G1) . e;
set v2 = (the_Source_of G2) . e;
set w2 = (the_Target_of G2) . e;
hereby :: thesis: ( ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
assume e Joins x,y,G1 ; :: thesis: e Joins x,y,G2
then ( e in the_Edges_of G1 & ( ( (the_Source_of G1) . e = x & (the_Target_of G1) . e = y ) or ( (the_Source_of G1) . e = y & (the_Target_of G1) . e = x ) ) ) by GLIB_000:def 13;
then A1: ( e in the_Edges_of G2 & ( ( (the_Source_of G1) . e = x & (the_Target_of G1) . e = y ) or ( (the_Source_of G1) . e = y & (the_Target_of G1) . e = x ) ) ) by GLIB_006:def 10;
then ( (the_Source_of G1) . e = (the_Source_of G2) . e & (the_Target_of G1) . e = (the_Target_of G2) . e ) by GLIB_006:def 9;
hence e Joins x,y,G2 by A1, GLIB_000:def 13; :: thesis: verum
end;
thus ( e Joins x,y,G2 implies e Joins x,y,G1 ) by GLIB_006:70; :: thesis: ( ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
hereby :: thesis: ( ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
assume e DJoins x,y,G1 ; :: thesis: e DJoins x,y,G2
then ( e in the_Edges_of G1 & (the_Source_of G1) . e = x & (the_Target_of G1) . e = y ) by GLIB_000:def 14;
then A2: ( e in the_Edges_of G2 & (the_Source_of G1) . e = x & (the_Target_of G1) . e = y ) by GLIB_006:def 10;
then ( (the_Source_of G1) . e = (the_Source_of G2) . e & (the_Target_of G1) . e = (the_Target_of G2) . e ) by GLIB_006:def 9;
hence e DJoins x,y,G2 by A2, GLIB_000:def 14; :: thesis: verum
end;
thus ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) by GLIB_006:70; :: thesis: ( ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
hereby :: thesis: ( ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
assume e SJoins x,y,G1 ; :: thesis: e SJoins x,y,G2
then ( e in the_Edges_of G1 & ( ( (the_Source_of G1) . e in x & (the_Target_of G1) . e in y ) or ( (the_Source_of G1) . e in y & (the_Target_of G1) . e in x ) ) ) by GLIB_000:def 15;
then A3: ( e in the_Edges_of G2 & ( ( (the_Source_of G1) . e in x & (the_Target_of G1) . e in y ) or ( (the_Source_of G1) . e in y & (the_Target_of G1) . e in x ) ) ) by GLIB_006:def 10;
then ( (the_Source_of G1) . e = (the_Source_of G2) . e & (the_Target_of G1) . e = (the_Target_of G2) . e ) by GLIB_006:def 9;
hence e SJoins x,y,G2 by A3, GLIB_000:def 15; :: thesis: verum
end;
thus ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) by GLIB_006:70; :: thesis: ( e DSJoins x,y,G1 iff e DSJoins x,y,G2 )
hereby :: thesis: ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 )
assume e DSJoins x,y,G1 ; :: thesis: e DSJoins x,y,G2
then ( e in the_Edges_of G1 & (the_Source_of G1) . e in x & (the_Target_of G1) . e in y ) by GLIB_000:def 16;
then A4: ( e in the_Edges_of G2 & (the_Source_of G1) . e in x & (the_Target_of G1) . e in y ) by GLIB_006:def 10;
then ( (the_Source_of G1) . e = (the_Source_of G2) . e & (the_Target_of G1) . e = (the_Target_of G2) . e ) by GLIB_006:def 9;
hence e DSJoins x,y,G2 by A4, GLIB_000:def 16; :: thesis: verum
end;
thus ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) by GLIB_006:70; :: thesis: verum