let G1 be _Graph; :: thesis: for G2 being Subgraph of G1

for E being RepEdgeSelection of G1 st E c= the_Edges_of G2 holds

E is RepEdgeSelection of G2

let G2 be Subgraph of G1; :: thesis: for E being RepEdgeSelection of G1 st E c= the_Edges_of G2 holds

E is RepEdgeSelection of G2

let E be RepEdgeSelection of G1; :: thesis: ( E c= the_Edges_of G2 implies E is RepEdgeSelection of G2 )

assume A1: E c= the_Edges_of G2 ; :: thesis: E is RepEdgeSelection of G2

for E being RepEdgeSelection of G1 st E c= the_Edges_of G2 holds

E is RepEdgeSelection of G2

let G2 be Subgraph of G1; :: thesis: for E being RepEdgeSelection of G1 st E c= the_Edges_of G2 holds

E is RepEdgeSelection of G2

let E be RepEdgeSelection of G1; :: thesis: ( E c= the_Edges_of G2 implies E is RepEdgeSelection of G2 )

assume A1: E c= the_Edges_of G2 ; :: thesis: E is RepEdgeSelection of G2

now :: thesis: for v, w, e0 being object st e0 Joins v,w,G2 holds

ex e being object st

( e Joins v,w,G2 & e in E & ( for e9 being object st e9 Joins v,w,G2 & e9 in E holds

e9 = e ) )

hence
E is RepEdgeSelection of G2
by A1, Def5; :: thesis: verumex e being object st

( e Joins v,w,G2 & e in E & ( for e9 being object st e9 Joins v,w,G2 & e9 in E holds

e9 = e ) )

let v, w, e0 be object ; :: thesis: ( e0 Joins v,w,G2 implies ex e being object st

( e Joins v,w,G2 & e in E & ( for e9 being object st e9 Joins v,w,G2 & e9 in E holds

e9 = e ) ) )

A2: ( v is set & w is set ) by TARSKI:1;

assume e0 Joins v,w,G2 ; :: thesis: ex e being object st

( e Joins v,w,G2 & e in E & ( for e9 being object st e9 Joins v,w,G2 & e9 in E holds

e9 = e ) )

then consider e being object such that

A3: ( e Joins v,w,G1 & e in E ) and

A4: for e9 being object st e9 Joins v,w,G1 & e9 in E holds

e9 = e by A2, Def5, GLIB_000:72;

take e = e; :: thesis: ( e Joins v,w,G2 & e in E & ( for e9 being object st e9 Joins v,w,G2 & e9 in E holds

e9 = e ) )

thus ( e Joins v,w,G2 & e in E ) by A1, A2, A3, GLIB_000:73; :: thesis: for e9 being object st e9 Joins v,w,G2 & e9 in E holds

e9 = e

let e9 be object ; :: thesis: ( e9 Joins v,w,G2 & e9 in E implies e9 = e )

assume ( e9 Joins v,w,G2 & e9 in E ) ; :: thesis: e9 = e

hence e9 = e by A2, A4, GLIB_000:72; :: thesis: verum

end;( e Joins v,w,G2 & e in E & ( for e9 being object st e9 Joins v,w,G2 & e9 in E holds

e9 = e ) ) )

A2: ( v is set & w is set ) by TARSKI:1;

assume e0 Joins v,w,G2 ; :: thesis: ex e being object st

( e Joins v,w,G2 & e in E & ( for e9 being object st e9 Joins v,w,G2 & e9 in E holds

e9 = e ) )

then consider e being object such that

A3: ( e Joins v,w,G1 & e in E ) and

A4: for e9 being object st e9 Joins v,w,G1 & e9 in E holds

e9 = e by A2, Def5, GLIB_000:72;

take e = e; :: thesis: ( e Joins v,w,G2 & e in E & ( for e9 being object st e9 Joins v,w,G2 & e9 in E holds

e9 = e ) )

thus ( e Joins v,w,G2 & e in E ) by A1, A2, A3, GLIB_000:73; :: thesis: for e9 being object st e9 Joins v,w,G2 & e9 in E holds

e9 = e

let e9 be object ; :: thesis: ( e9 Joins v,w,G2 & e9 in E implies e9 = e )

assume ( e9 Joins v,w,G2 & e9 in E ) ; :: thesis: e9 = e

hence e9 = e by A2, A4, GLIB_000:72; :: thesis: verum