let G1 be _Graph; :: thesis: for E1 being RepDEdgeSelection of G1
for G2 being inducedSubgraph of G1, the_Vertices_of G1,E1
for E2 being RepEdgeSelection of G2 holds
( E2 c= E1 & E2 is RepEdgeSelection of G1 )
let E1 be RepDEdgeSelection of G1; :: thesis: for G2 being inducedSubgraph of G1, the_Vertices_of G1,E1
for E2 being RepEdgeSelection of G2 holds
( E2 c= E1 & E2 is RepEdgeSelection of G1 )
let G2 be inducedSubgraph of G1, the_Vertices_of G1,E1; :: thesis: for E2 being RepEdgeSelection of G2 holds
( E2 c= E1 & E2 is RepEdgeSelection of G1 )
let E2 be RepEdgeSelection of G2; :: thesis: ( E2 c= E1 & E2 is RepEdgeSelection of G1 )
( the_Vertices_of G1 c= the_Vertices_of G1 & the_Edges_of G1 = G1 .edgesBetween (the_Vertices_of G1) ) by GLIB_000:34;
then A1: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = E1 ) by GLIB_000:def 37;
hence E2 c= E1 ; :: thesis: E2 is RepEdgeSelection of G1
then A2: E2 c= the_Edges_of G1 by XBOOLE_1:1;
now :: thesis: for v, w, e0 being object st e0 Joins v,w,G1 holds
ex e2 being object st
( e2 Joins v,w,G1 & e2 in E2 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E2 holds
e9 = e2 ) )
let v, w, e0 be object ; :: thesis: ( e0 Joins v,w,G1 implies ex e2 being object st
( e2 Joins v,w,G1 & e2 in E2 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E2 holds
e9 = e2 ) ) )
A3: ( v is set & w is set ) by TARSKI:1;
assume A4: e0 Joins v,w,G1 ; :: thesis: ex e2 being object st
( e2 Joins v,w,G1 & e2 in E2 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E2 holds
e9 = e2 ) )
ex e1 being object st e1 Joins v,w,G2
proof
per cases ( e0 DJoins v,w,G1 or e0 DJoins w,v,G1 ) by A4, GLIB_000:16;
suppose e0 DJoins v,w,G1 ; :: thesis: ex e1 being object st e1 Joins v,w,G2
then consider e1 being object such that
A5: ( e1 DJoins v,w,G1 & e1 in E1 ) and
for e9 being object st e9 DJoins v,w,G1 & e9 in E1 holds
e9 = e1 by Def6;
take e1 ; :: thesis: e1 Joins v,w,G2
e1 DJoins v,w,G2 by A1, A3, A5, GLIB_000:73;
hence e1 Joins v,w,G2 by GLIB_000:16; :: thesis: verum
end;
suppose e0 DJoins w,v,G1 ; :: thesis: ex e1 being object st e1 Joins v,w,G2
then consider e1 being object such that
A6: ( e1 DJoins w,v,G1 & e1 in E1 ) and
for e9 being object st e9 DJoins w,v,G1 & e9 in E1 holds
e9 = e1 by Def6;
take e1 ; :: thesis: e1 Joins v,w,G2
e1 DJoins w,v,G2 by A3, A1, A6, GLIB_000:73;
hence e1 Joins v,w,G2 by GLIB_000:16; :: thesis: verum
end;
end;
end;
then consider e1 being object such that
A7: e1 Joins v,w,G2 ;
consider e2 being object such that
A8: ( e2 Joins v,w,G2 & e2 in E2 ) and
A9: for e9 being object st e9 Joins v,w,G2 & e9 in E2 holds
e9 = e2 by A7, Def5;
take e2 = e2; :: thesis: ( e2 Joins v,w,G1 & e2 in E2 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E2 holds
e9 = e2 ) )
thus ( e2 Joins v,w,G1 & e2 in E2 ) by A3, A8, GLIB_000:72; :: thesis: for e9 being object st e9 Joins v,w,G1 & e9 in E2 holds
e9 = e2
let e9 be object ; :: thesis: ( e9 Joins v,w,G1 & e9 in E2 implies e9 = e2 )
assume A10: ( e9 Joins v,w,G1 & e9 in E2 ) ; :: thesis: e9 = e2
e9 Joins v,w,G2 by A3, A10, GLIB_000:73;
hence e9 = e2 by A9, A10; :: thesis: verum
end;
hence E2 is RepEdgeSelection of G1 by A2, Def5; :: thesis: verum