let G1 be _Graph; :: thesis: for E1 being RepEdgeSelection of G1

for G2 being inducedSubgraph of G1, the_Vertices_of G1,E1

for E2 being RepEdgeSelection of G2 holds E1 = E2

let E1 be RepEdgeSelection of G1; :: thesis: for G2 being inducedSubgraph of G1, the_Vertices_of G1,E1

for E2 being RepEdgeSelection of G2 holds E1 = E2

let G2 be inducedSubgraph of G1, the_Vertices_of G1,E1; :: thesis: for E2 being RepEdgeSelection of G2 holds E1 = E2

let E2 be RepEdgeSelection of G2; :: thesis: E1 = E2

( the_Edges_of G1 = G1 .edgesBetween (the_Vertices_of G1) & the_Vertices_of G1 c= the_Vertices_of G1 ) by GLIB_000:34;

then A1: the_Edges_of G2 = E1 by GLIB_000:def 37;

for e being object st e in E1 holds

e in E2

hence E1 = E2 by A1, XBOOLE_0:def 10; :: thesis: verum

for G2 being inducedSubgraph of G1, the_Vertices_of G1,E1

for E2 being RepEdgeSelection of G2 holds E1 = E2

let E1 be RepEdgeSelection of G1; :: thesis: for G2 being inducedSubgraph of G1, the_Vertices_of G1,E1

for E2 being RepEdgeSelection of G2 holds E1 = E2

let G2 be inducedSubgraph of G1, the_Vertices_of G1,E1; :: thesis: for E2 being RepEdgeSelection of G2 holds E1 = E2

let E2 be RepEdgeSelection of G2; :: thesis: E1 = E2

( the_Edges_of G1 = G1 .edgesBetween (the_Vertices_of G1) & the_Vertices_of G1 c= the_Vertices_of G1 ) by GLIB_000:34;

then A1: the_Edges_of G2 = E1 by GLIB_000:def 37;

for e being object st e in E1 holds

e in E2

proof

then
E1 c= E2
by TARSKI:def 3;
let e be object ; :: thesis: ( e in E1 implies e in E2 )

assume A2: e in E1 ; :: thesis: e in E2

set v = (the_Source_of G2) . e;

set w = (the_Target_of G2) . e;

A3: e Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G2 by A1, A2, GLIB_000:def 13;

then consider e2 being object such that

A4: ( e2 Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G2 & e2 in E2 ) and

for e9 being object st e9 Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G2 & e9 in E2 holds

e9 = e2 by Def5;

A5: e Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G1 by A3, GLIB_000:72;

then consider e1 being object such that

( e1 Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G1 & e1 in E1 ) and

A6: for e9 being object st e9 Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G1 & e9 in E1 holds

e9 = e1 by Def5;

e = e1 by A2, A5, A6;

hence e in E2 by A1, A4, A6, GLIB_000:72; :: thesis: verum

end;assume A2: e in E1 ; :: thesis: e in E2

set v = (the_Source_of G2) . e;

set w = (the_Target_of G2) . e;

A3: e Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G2 by A1, A2, GLIB_000:def 13;

then consider e2 being object such that

A4: ( e2 Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G2 & e2 in E2 ) and

for e9 being object st e9 Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G2 & e9 in E2 holds

e9 = e2 by Def5;

A5: e Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G1 by A3, GLIB_000:72;

then consider e1 being object such that

( e1 Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G1 & e1 in E1 ) and

A6: for e9 being object st e9 Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G1 & e9 in E1 holds

e9 = e1 by Def5;

e = e1 by A2, A5, A6;

hence e in E2 by A1, A4, A6, GLIB_000:72; :: thesis: verum

hence E1 = E2 by A1, XBOOLE_0:def 10; :: thesis: verum