let G1 be _Graph; :: thesis: for G2 being Subgraph of G1
for x, y, e being object st e Joins x,y,G2 holds
e Joins x,y,G1
let G2 be Subgraph of G1; :: thesis: for x, y, e being object st e Joins x,y,G2 holds
e Joins x,y,G1
let x, y, e be object ; :: thesis: ( e Joins x,y,G2 implies e Joins x,y,G1 )
assume A1: e Joins x,y,G2 ; :: thesis: e Joins x,y,G1
then A2: e in the_Edges_of G2 ;
( ( (the_Source_of G2) . e = x & (the_Target_of G2) . e = y ) or ( (the_Source_of G2) . e = y & (the_Target_of G2) . e = x ) ) by A1;
then ( ( (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 A2, Def32;
hence e Joins x,y,G1 by A2; :: thesis: verum