let G be _Graph; :: thesis: card (Class (EdgeAdjEqRel G)) c= card (VertexAdjSymRel G)
set R = VertexAdjSymRel G;
defpred S1[ object , object ] means ex e being object st
( e Joins $1 `1 ,$1 `2 ,G & $2 = Class ((EdgeAdjEqRel G),e) );
A1: for x, y1, y2 being object st x in VertexAdjSymRel G & S1[x,y1] & S1[x,y2] holds
y1 = y2
proof
let x, y1, y2 be object ; :: thesis: ( x in VertexAdjSymRel G & S1[x,y1] & S1[x,y2] implies y1 = y2 )
assume A2: ( x in VertexAdjSymRel G & S1[x,y1] & S1[x,y2] ) ; :: thesis: y1 = y2
then consider e1 being object such that
A3: ( e1 Joins x `1 ,x `2 ,G & y1 = Class ((EdgeAdjEqRel G),e1) ) ;
consider e2 being object such that
A4: ( e2 Joins x `1 ,x `2 ,G & y2 = Class ((EdgeAdjEqRel G),e2) ) by A2;
[e1,e2] in EdgeAdjEqRel G by A3, A4, GLIB_009:def 3;
then A5: e2 in Class ((EdgeAdjEqRel G),e1) by EQREL_1:18;
e1 in the_Edges_of G by A3, GLIB_000:def 13;
hence y1 = y2 by A3, A4, A5, EQREL_1:23; :: thesis: verum
end;
A6: for x being object st x in VertexAdjSymRel G holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in VertexAdjSymRel G implies ex y being object st S1[x,y] )
assume A7: x in VertexAdjSymRel G ; :: thesis: ex y being object st S1[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 Joins v,w,G by A7, A8, Th32;
take Class ((EdgeAdjEqRel G),e) ; :: thesis: S1[x, Class ((EdgeAdjEqRel G),e)]
take e ; :: thesis: ( e Joins x `1 ,x `2 ,G & Class ((EdgeAdjEqRel G),e) = Class ((EdgeAdjEqRel G),e) )
thus ( e Joins x `1 ,x `2 ,G & Class ((EdgeAdjEqRel G),e) = Class ((EdgeAdjEqRel G),e) ) by A8, A9; :: thesis: verum
end;
consider f being Function such that
A10: ( dom f = VertexAdjSymRel G & ( for x being object st x in VertexAdjSymRel G holds
S1[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 (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
A11: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
consider e being object such that
A12: ( e Joins x `1 ,x `2 ,G & y = Class ((EdgeAdjEqRel G),e) ) by A10, A11;
e in the_Edges_of G by A12, GLIB_000:def 13;
hence y in Class (EdgeAdjEqRel G) by A12, EQREL_1:def 3; :: thesis: verum
end;
assume y in Class (EdgeAdjEqRel G) ; :: thesis: y in rng f
then consider e being object such that
A13: ( e in the_Edges_of G & y = Class ((EdgeAdjEqRel G),e) ) by EQREL_1:def 3;
set x = [((the_Source_of G) . e),((the_Target_of G) . e)];
A14: e Joins [((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 13;
then A15: [((the_Source_of G) . e),((the_Target_of G) . e)] in VertexAdjSymRel G by Th32;
then S1[[((the_Source_of G) . e),((the_Target_of G) . e)],f . [((the_Source_of G) . e),((the_Target_of G) . e)]] by A10;
then f . [((the_Source_of G) . e),((the_Target_of G) . e)] = y by A1, A13, A14, A15;
hence y in rng f by A10, A15, FUNCT_1:3; :: thesis: verum
end;
then rng f = Class (EdgeAdjEqRel G) by TARSKI:2;
hence card (Class (EdgeAdjEqRel G)) c= card (VertexAdjSymRel G) by A10, CARD_1:12; :: thesis: verum