let G1 be _Graph; :: thesis: for G2 being Subgraph of G1
for x, y, e being set st e in the_Edges_of G2 holds
( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) )
let G2 be Subgraph of G1; :: thesis: for x, y, e being set st e in the_Edges_of G2 holds
( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) )
let x, y, e be set ; :: thesis: ( e in the_Edges_of G2 implies ( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) ) )
assume A1: e in the_Edges_of G2 ; :: thesis: ( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) )

hereby :: thesis: ( ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) )

assume e Joins x,y,G1 ; :: thesis: e Joins x,y,G2
then A2: ( ( (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 Def15;
( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) by A1, Def34;
hence e Joins x,y,G2 by A1, A2, Def15; :: thesis: verum

end;

(the_Target_of G2) . e = ((the_Target_of G1) | (the_Edges_of G2)) . e by Th48;
then A3: (the_Target_of G2) . e = (the_Target_of G1) . e by A1, FUNCT_1:49;

hereby :: thesis: ( ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) )

assume A4: e DJoins x,y,G1 ; :: thesis: e DJoins x,y,G2
then (the_Target_of G1) . e = y by Def16;
then A5: (the_Target_of G2) . e = y by A1, Def34;
(the_Source_of G1) . e = x by A4, Def16;
then (the_Source_of G2) . e = x by A1, Def34;
hence e DJoins x,y,G2 by A1, A5, Def16; :: thesis: verum

end;

hereby :: thesis: ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 )

(the_Target_of G2) . e = ((the_Target_of G1) | (the_Edges_of G2)) . e by Th48;
then A6: (the_Target_of G2) . e = (the_Target_of G1) . e by A1, FUNCT_1:49;
assume e SJoins x,y,G1 ; :: thesis: e SJoins x,y,G2
then A7: ( ( (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 Def17;
(the_Source_of G2) . e = ((the_Source_of G1) | (the_Edges_of G2)) . e by Th48;
then (the_Source_of G2) . e = (the_Source_of G1) . e by A1, FUNCT_1:49;
hence e SJoins x,y,G2 by A1, A7, A6, Def17; :: thesis: verum

end;

assume e DSJoins x,y,G1 ; :: thesis: e DSJoins x,y,G2
then A8: ( (the_Source_of G1) . e in x & (the_Target_of G1) . e in y ) by Def18;
(the_Source_of G2) . e = ((the_Source_of G1) | (the_Edges_of G2)) . e by Th48;
then (the_Source_of G2) . e = (the_Source_of G1) . e by A1, FUNCT_1:49;
hence e DSJoins x,y,G2 by A1, A8, A3, Def18; :: thesis: verum