let G be _Graph; :: thesis: for E being RepEdgeSelection of G holds card E = card (Class (EdgeAdjEqRel G))
let E be RepEdgeSelection of G; :: thesis: card E = card (Class (EdgeAdjEqRel G))
deffunc H₁( object ) -> Element of bool (the_Edges_of G) = Class ((EdgeAdjEqRel 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 (EdgeAdjEqRel G) ) & ( y in Class (EdgeAdjEqRel G) implies y in rng f ) )

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

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

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

end;

assume y in Class (EdgeAdjEqRel G) ; :: thesis: y in rng f
then consider x being object such that
A3: ( x in the_Edges_of G & y = Class ((EdgeAdjEqRel G),x) ) by EQREL_1:def 3;
set v = (the_Source_of G) . x;
set w = (the_Target_of G) . x;
A4: x Joins (the_Source_of G) . x,(the_Target_of G) . x,G by A3, GLIB_000:def 13;
then consider e being object such that
A5: ( e Joins (the_Source_of G) . x,(the_Target_of G) . x,G & e in E ) and
for e9 being object st e9 Joins (the_Source_of G) . x,(the_Target_of G) . x,G & e9 in E holds
e9 = e by GLIB_009:def 5;
[x,e] in EdgeAdjEqRel G by A4, A5, GLIB_009:def 3;
then e in Class ((EdgeAdjEqRel G),x) by EQREL_1:18;
then y = Class ((EdgeAdjEqRel 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 (EdgeAdjEqRel 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 ((EdgeAdjEqRel G),x1) & f . x2 = Class ((EdgeAdjEqRel G),x2) ) by A1;
then x2 in Class ((EdgeAdjEqRel G),x1) by A1, A7, EQREL_1:23;
then [x1,x2] in EdgeAdjEqRel G by EQREL_1:18;
then consider v, w being object such that
A8: ( x1 Joins v,w,G & x2 Joins v,w,G ) by GLIB_009:def 3;
consider e being object such that
( e Joins v,w,G & e in E ) and
A9: for e9 being object st e9 Joins v,w,G & e9 in E holds
e9 = e by A8, GLIB_009:def 5;
( x1 = e & x2 = e ) by A1, A7, A8, A9;
hence x1 = x2 ; :: thesis: verum

end;

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