let G be _Graph; :: thesis: card (VertexDomRel G) = card (Class (DEdgeAdjEqRel G))
set R = VertexDomRel G;
defpred S₁[ object , object ] means ex e being object st
( e DJoins $1 `1 ,$1 `2 ,G & $2 = Class ((DEdgeAdjEqRel G),e) );
A1: for x, y1, y2 being object st x in VertexDomRel G & S₁[x,y1] & S₁[x,y2] holds
y1 = y2

proof

let x, y1, y2 be object ; :: thesis: ( x in VertexDomRel G & S₁[x,y1] & S₁[x,y2] implies y1 = y2 )
assume A2: ( x in VertexDomRel G & S₁[x,y1] & S₁[x,y2] ) ; :: thesis: y1 = y2
then consider e1 being object such that
A3: ( e1 DJoins x `1 ,x `2 ,G & y1 = Class ((DEdgeAdjEqRel G),e1) ) ;
consider e2 being object such that
A4: ( e2 DJoins x `1 ,x `2 ,G & y2 = Class ((DEdgeAdjEqRel G),e2) ) by A2;
[e1,e2] in DEdgeAdjEqRel G by A3, A4, GLIB_009:def 4;
then A5: e2 in Class ((DEdgeAdjEqRel G),e1) by EQREL_1:18;
e1 in the_Edges_of G by A3, GLIB_000:def 14;
hence y1 = y2 by A3, A4, A5, EQREL_1:23; :: thesis: verum

end;

A6: for x being object st x in VertexDomRel G holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in VertexDomRel G implies ex y being object st S₁[x,y] )
assume A7: x in VertexDomRel G ; :: thesis: ex y being object st S₁[x,y]
then consider v, w being object such that
A8: x = [v,w] by RELAT_1:def 1;
consider e being object such that
A9: e DJoins v,w,G by A7, A8, Th1;
take Class ((DEdgeAdjEqRel G),e) ; :: thesis: S₁[x, Class ((DEdgeAdjEqRel G),e)]
take e ; :: thesis: ( e DJoins x `1 ,x `2 ,G & Class ((DEdgeAdjEqRel G),e) = Class ((DEdgeAdjEqRel G),e) )
thus ( e DJoins x `1 ,x `2 ,G & Class ((DEdgeAdjEqRel G),e) = Class ((DEdgeAdjEqRel G),e) ) by A8, A9; :: thesis: verum

end;

consider f being Function such that
A10: ( dom f = VertexDomRel G & ( for x being object st x in VertexDomRel G holds
S₁[x,f . x] ) ) from FUNCT_1:sch 2(A1, A6);

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
A11: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
consider e being object such that
A12: ( e DJoins x `1 ,x `2 ,G & y = Class ((DEdgeAdjEqRel G),e) ) by A10, A11;
e in the_Edges_of G by A12, GLIB_000:def 14;
hence y in Class (DEdgeAdjEqRel G) by A12, EQREL_1:def 3; :: thesis: verum

end;

assume y in Class (DEdgeAdjEqRel G) ; :: thesis: y in rng f
then consider e being object such that
A13: ( e in the_Edges_of G & y = Class ((DEdgeAdjEqRel G),e) ) by EQREL_1:def 3;
set x = [((the_Source_of G) . e),((the_Target_of G) . e)];
A14: e DJoins [((the_Source_of G) . e),((the_Target_of G) . e)] `1 ,[((the_Source_of G) . e),((the_Target_of G) . e)] `2 ,G by A13, GLIB_000:def 14;
then S₁[[((the_Source_of G) . e),((the_Target_of G) . e)],f . [((the_Source_of G) . e),((the_Target_of G) . e)]] by A10, Th1;
then f . [((the_Source_of G) . e),((the_Target_of G) . e)] = y by A1, A13, A14, Th1;
hence y in rng f by A10, A14, Th1, FUNCT_1:3; :: thesis: verum

end;

then A16: rng f = Class (DEdgeAdjEqRel G) by TARSKI:2;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A17: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then consider e1 being object such that
A18: ( e1 DJoins x1 `1 ,x1 `2 ,G & f . x1 = Class ((DEdgeAdjEqRel G),e1) ) by A10;
consider e2 being object such that
A19: ( e2 DJoins x2 `1 ,x2 `2 ,G & f . x2 = Class ((DEdgeAdjEqRel G),e2) ) by A10, A17;
e1 in the_Edges_of G by A18, GLIB_000:def 14;
then e2 in Class ((DEdgeAdjEqRel G),e1) by A17, A18, A19, EQREL_1:23;
then [e1,e2] in DEdgeAdjEqRel G by EQREL_1:18;
then consider v, w being object such that
A20: ( e1 DJoins v,w,G & e2 DJoins v,w,G ) by GLIB_009:def 4;
( v = x1 `1 & w = x1 `2 & v = x2 `1 & w = x2 `2 ) by A18, A19, A20, GLIB_000:125;
then A21: [(x1 `1),(x1 `2)] = [(x2 `1),(x2 `2)] ;
( ex a, b being object st x1 = [a,b] & ex a, b being object st x2 = [a,b] ) by A10, A17, RELAT_1:def 1;
hence x1 = x2 by A21; :: thesis: verum

end;

hence card (VertexDomRel G) = card (Class (DEdgeAdjEqRel G)) by A10, A16, FUNCT_1:def 4, CARD_1:70; :: thesis: verum