let G be _Graph; :: thesis: for V being set
for H being addVertices of G,V
for E being Subset of (the_Edges_of G) holds
( E is RepEdgeSelection of G iff E is RepEdgeSelection of H )
let V be set ; :: thesis: for H being addVertices of G,V
for E being Subset of (the_Edges_of G) holds
( E is RepEdgeSelection of G iff E is RepEdgeSelection of H )
let H be addVertices of G,V; :: thesis: for E being Subset of (the_Edges_of G) holds
( E is RepEdgeSelection of G iff E is RepEdgeSelection of H )
let E be Subset of (the_Edges_of G); :: thesis: ( E is RepEdgeSelection of G iff E is RepEdgeSelection of H )
A1: the_Edges_of G = the_Edges_of H by GLIB_006:def 10;

hereby :: thesis: ( E is RepEdgeSelection of H implies E is RepEdgeSelection of G )

assume A2: E is RepEdgeSelection of G ; :: thesis: E is RepEdgeSelection of H

now :: thesis: for v, w, e0 being object st e0 Joins v,w,H holds
ex e being object st
( e Joins v,w,H & e in E & ( for e9 being object st e9 Joins v,w,H & e9 in E holds
e9 = e ) )

let v, w, e0 be object ; :: thesis: ( e0 Joins v,w,H implies ex e being object st
( e Joins v,w,H & e in E & ( for e9 being object st e9 Joins v,w,H & e9 in E holds
e9 = e ) ) )
A3: ( v is set & w is set ) by TARSKI:1;
assume e0 Joins v,w,H ; :: thesis: ex e being object st
( e Joins v,w,H & e in E & ( for e9 being object st e9 Joins v,w,H & e9 in E holds
e9 = e ) )
then consider e being object such that
A4: ( e Joins v,w,G & e in E ) and
A5: for e9 being object st e9 Joins v,w,G & e9 in E holds
e9 = e by A2, A3, GLIB_009:41, GLIB_009:def 5;
take e = e; :: thesis: ( e Joins v,w,H & e in E & ( for e9 being object st e9 Joins v,w,H & e9 in E holds
e9 = e ) )
thus ( e Joins v,w,H & e in E ) by A3, A4, GLIB_009:41; :: thesis: for e9 being object st e9 Joins v,w,H & e9 in E holds
e9 = e
let e9 be object ; :: thesis: ( e9 Joins v,w,H & e9 in E implies e9 = e )
assume ( e9 Joins v,w,H & e9 in E ) ; :: thesis: e9 = e
hence e9 = e by A3, A5, GLIB_009:41; :: thesis: verum

end;

hence E is RepEdgeSelection of H by A1, GLIB_009:def 5; :: thesis: verum

end;

assume A6: E is RepEdgeSelection of H ; :: thesis: E is RepEdgeSelection of G

now :: thesis: for v, w, e0 being object st e0 Joins v,w,G holds
ex e being object st
( e Joins v,w,G & e in E & ( for e9 being object st e9 Joins v,w,G & e9 in E holds
e9 = e ) )

let v, w, e0 be object ; :: thesis: ( e0 Joins v,w,G implies ex e being object st
( e Joins v,w,G & e in E & ( for e9 being object st e9 Joins v,w,G & e9 in E holds
e9 = e ) ) )
A7: ( v is set & w is set ) by TARSKI:1;
assume e0 Joins v,w,G ; :: thesis: ex e being object st
( e Joins v,w,G & e in E & ( for e9 being object st e9 Joins v,w,G & e9 in E holds
e9 = e ) )
then consider e being object such that
A8: ( e Joins v,w,H & e in E ) and
A9: for e9 being object st e9 Joins v,w,H & e9 in E holds
e9 = e by A6, A7, GLIB_009:41, GLIB_009:def 5;
take e = e; :: thesis: ( e Joins v,w,G & e in E & ( for e9 being object st e9 Joins v,w,G & e9 in E holds
e9 = e ) )
thus ( e Joins v,w,G & e in E ) by A7, A8, GLIB_009:41; :: thesis: for e9 being object st e9 Joins v,w,G & e9 in E holds
e9 = e
let e9 be object ; :: thesis: ( e9 Joins v,w,G & e9 in E implies e9 = e )
assume ( e9 Joins v,w,G & e9 in E ) ; :: thesis: e9 = e
hence e9 = e by A7, A9, GLIB_009:41; :: thesis: verum

end;

hence E is RepEdgeSelection of G by GLIB_009:def 5; :: thesis: verum