let G1 be _Graph; :: thesis: for G2 being Subgraph of G1
for x, y being set
for e being object holds
( ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
let G2 be Subgraph of G1; :: thesis: for x, y being set
for e being object holds
( ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( 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,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
let e be object ; :: thesis: ( ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
thus ( e Joins x,y,G2 implies e Joins x,y,G1 ) by Lm4; :: thesis: ( ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( 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,G2 implies e DSJoins x,y,G1 ) )
assume A1: e DJoins x,y,G2 ; :: thesis: e DJoins x,y,G1
then A2: e in the_Edges_of G2 ;
(the_Target_of G2) . e = y by A1;
then A3: (the_Target_of G1) . e = y by A2, Def32;
(the_Source_of G2) . e = x by A1;
then (the_Source_of G1) . e = x by A2, Def32;
hence e DJoins x,y,G1 by A2, A3; :: thesis: verum
end;
hereby :: thesis: ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 )
assume A4: e SJoins x,y,G2 ; :: thesis: e SJoins x,y,G1
then A5: ( ( (the_Source_of G2) . e in x & (the_Target_of G2) . e in y ) or ( (the_Source_of G2) . e in y & (the_Target_of G2) . e in x ) ) ;
A6: e in the_Edges_of G2 by A4;
then ( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) by Def32;
hence e SJoins x,y,G1 by A6, A5; :: thesis: verum
end;
assume A7: e DSJoins x,y,G2 ; :: thesis: e DSJoins x,y,G1
then A8: ( (the_Source_of G2) . e in x & (the_Target_of G2) . e in y ) ;
A9: e in the_Edges_of G2 by A7;
then ( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) by Def32;
hence e DSJoins x,y,G1 by A9, A8; :: thesis: verum