let G be _Graph; for V being set
for H being addVertices of G,V
for E being Subset of (the_Edges_of G) holds
( E is RepDEdgeSelection of G iff E is RepDEdgeSelection of H )
let V be set ; for H being addVertices of G,V
for E being Subset of (the_Edges_of G) holds
( E is RepDEdgeSelection of G iff E is RepDEdgeSelection of H )
let H be addVertices of G,V; for E being Subset of (the_Edges_of G) holds
( E is RepDEdgeSelection of G iff E is RepDEdgeSelection of H )
let E be Subset of (the_Edges_of G); ( E is RepDEdgeSelection of G iff E is RepDEdgeSelection of H )
A1:
the_Edges_of G = the_Edges_of H
by GLIB_006:def 10;
hereby ( E is RepDEdgeSelection of H implies E is RepDEdgeSelection of G )
assume A2:
E is
RepDEdgeSelection of
G
;
E is RepDEdgeSelection of Hnow for v, w, e0 being object st e0 DJoins v,w,H holds
ex e being object st
( e DJoins v,w,H & e in E & ( for e9 being object st e9 DJoins v,w,H & e9 in E holds
e9 = e ) )let v,
w,
e0 be
object ;
( e0 DJoins v,w,H implies ex e being object st
( e DJoins v,w,H & e in E & ( for e9 being object st e9 DJoins v,w,H & e9 in E holds
e9 = e ) ) )A3:
(
v is
set &
w is
set )
by TARSKI:1;
assume
e0 DJoins v,
w,
H
;
ex e being object st
( e DJoins v,w,H & e in E & ( for e9 being object st e9 DJoins v,w,H & e9 in E holds
e9 = e ) )then consider e being
object such that A4:
(
e DJoins v,
w,
G &
e in E )
and A5:
for
e9 being
object st
e9 DJoins v,
w,
G &
e9 in E holds
e9 = e
by A2, A3, GLIB_009:41, GLIB_009:def 6;
take e =
e;
( e DJoins v,w,H & e in E & ( for e9 being object st e9 DJoins v,w,H & e9 in E holds
e9 = e ) )thus
(
e DJoins v,
w,
H &
e in E )
by A3, A4, GLIB_009:41;
for e9 being object st e9 DJoins v,w,H & e9 in E holds
e9 = elet e9 be
object ;
( e9 DJoins v,w,H & e9 in E implies e9 = e )assume
(
e9 DJoins v,
w,
H &
e9 in E )
;
e9 = ehence
e9 = e
by A3, A5, GLIB_009:41;
verum end; hence
E is
RepDEdgeSelection of
H
by A1, GLIB_009:def 6;
verum
end;
assume A6:
E is RepDEdgeSelection of H
; E is RepDEdgeSelection of G
now for v, w, e0 being object st e0 DJoins v,w,G holds
ex e being object st
( e DJoins v,w,G & e in E & ( for e9 being object st e9 DJoins v,w,G & e9 in E holds
e9 = e ) )let v,
w,
e0 be
object ;
( e0 DJoins v,w,G implies ex e being object st
( e DJoins v,w,G & e in E & ( for e9 being object st e9 DJoins v,w,G & e9 in E holds
e9 = e ) ) )A7:
(
v is
set &
w is
set )
by TARSKI:1;
assume
e0 DJoins v,
w,
G
;
ex e being object st
( e DJoins v,w,G & e in E & ( for e9 being object st e9 DJoins v,w,G & e9 in E holds
e9 = e ) )then consider e being
object such that A8:
(
e DJoins v,
w,
H &
e in E )
and A9:
for
e9 being
object st
e9 DJoins v,
w,
H &
e9 in E holds
e9 = e
by A6, A7, GLIB_009:41, GLIB_009:def 6;
take e =
e;
( e DJoins v,w,G & e in E & ( for e9 being object st e9 DJoins v,w,G & e9 in E holds
e9 = e ) )thus
(
e DJoins v,
w,
G &
e in E )
by A7, A8, GLIB_009:41;
for e9 being object st e9 DJoins v,w,G & e9 in E holds
e9 = elet e9 be
object ;
( e9 DJoins v,w,G & e9 in E implies e9 = e )assume
(
e9 DJoins v,
w,
G &
e9 in E )
;
e9 = ehence
e9 = e
by A7, A9, GLIB_009:41;
verum end;
hence
E is RepDEdgeSelection of G
by GLIB_009:def 6; verum