let G be _Graph; :: thesis: for E being RepDEdgeSelection of G holds card E = card (Class (DEdgeAdjEqRel G))
let E be RepDEdgeSelection of G; :: thesis: card E = card (Class (DEdgeAdjEqRel G))
deffunc H₁( object ) -> Element of bool (the_Edges_of G) = Class ((DEdgeAdjEqRel G),$1);
consider f being Function such that
A1: ( dom f = E & ( for x being object st x in E holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();

now :: thesis: for y being object holds
( ( y in rng f implies y in Class (DEdgeAdjEqRel G) ) & ( y in Class (DEdgeAdjEqRel G) implies y in rng f ) )

let y be object ; :: thesis: ( ( y in rng f implies y in Class (DEdgeAdjEqRel G) ) & ( y in Class (DEdgeAdjEqRel G) implies y in rng f ) )

hereby :: thesis: ( y in Class (DEdgeAdjEqRel G) implies y in rng f )

assume y in rng f ; :: thesis: y in Class (DEdgeAdjEqRel G)
then consider x being object such that
A2: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
y = Class ((DEdgeAdjEqRel G),x) by A1, A2;
hence y in Class (DEdgeAdjEqRel G) by A1, A2, EQREL_1:def 3; :: thesis: verum

end;

assume y in Class (DEdgeAdjEqRel G) ; :: thesis: y in rng f
then consider x being object such that
A3: ( x in the_Edges_of G & y = Class ((DEdgeAdjEqRel G),x) ) by EQREL_1:def 3;
set v = (the_Source_of G) . x;
set w = (the_Target_of G) . x;
A4: x DJoins (the_Source_of G) . x,(the_Target_of G) . x,G by A3, GLIB_000:def 14;
then consider e being object such that
A5: ( e DJoins (the_Source_of G) . x,(the_Target_of G) . x,G & e in E ) and
for e9 being object st e9 DJoins (the_Source_of G) . x,(the_Target_of G) . x,G & e9 in E holds
e9 = e by GLIB_009:def 6;
[x,e] in DEdgeAdjEqRel G by A4, A5, GLIB_009:def 4;
then e in Class ((DEdgeAdjEqRel G),x) by EQREL_1:18;
then y = Class ((DEdgeAdjEqRel G),e) by A3, EQREL_1:23
.= f . e by A1, A5 ;
hence y in rng f by A1, A5, FUNCT_1:3; :: thesis: verum

end;

then A6: rng f = Class (DEdgeAdjEqRel G) by TARSKI:2;

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A7: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then ( f . x1 = Class ((DEdgeAdjEqRel G),x1) & f . x2 = Class ((DEdgeAdjEqRel G),x2) ) by A1;
then x2 in Class ((DEdgeAdjEqRel G),x1) by A1, A7, EQREL_1:23;
then [x1,x2] in DEdgeAdjEqRel G by EQREL_1:18;
then consider v, w being object such that
A8: ( x1 DJoins v,w,G & x2 DJoins v,w,G ) by GLIB_009:def 4;
consider e being object such that
( e DJoins v,w,G & e in E ) and
A9: for e9 being object st e9 DJoins v,w,G & e9 in E holds
e9 = e by A8, GLIB_009:def 6;
( x1 = e & x2 = e ) by A1, A7, A8, A9;
hence x1 = x2 ; :: thesis: verum

end;

hence card E = card (Class (DEdgeAdjEqRel G)) by A1, A6, CARD_1:70, FUNCT_1:def 4; :: thesis: verum