proof

let x, y1, y2 be object ; :: thesis:
assume A4: ( x in the_Edges_of G & S₁[x,y1] & S₁[x,y2] ) ; :: thesis:
set v = (the_Source_of G) . x;
set w = (the_Target_of G) . x;

per cases by A4;

suppose ( y1 = [((the_Source_of G) . x),((the_Target_of G) . x)] & y2 = [((the_Source_of G) . x),((the_Target_of G) . x)] ) ; :: thesis:

hence y1 = y2 ; :: thesis:

end;

suppose A5: ( y1 = [((the_Source_of G) . x),((the_Target_of G) . x)] & y2 = [((the_Target_of G) . x),((the_Source_of G) . x)] ) ; :: thesis:

A6: ( y1 in the_Edges_of G9 & y2 in the_Edges_of G9 ) by A2, A4;
then ( y1 in the_Edges_of (createGraph ((the_Vertices_of G),(VertexAdjSymRel G))) & y2 in the_Edges_of (createGraph ((the_Vertices_of G),(VertexAdjSymRel G))) ) ;
then ( y1 in VertexAdjSymRel G & y2 in VertexAdjSymRel G ) ;
then ( y1 DJoins (the_Source_of G) . x,(the_Target_of G) . x, createGraph ((the_Vertices_of G),(VertexAdjSymRel G)) & y2 DJoins (the_Target_of G) . x,(the_Source_of G) . x, createGraph ((the_Vertices_of G),(VertexAdjSymRel G)) ) by A5, Th63;
then A7: ( y1 Joins (the_Source_of G) . x,(the_Target_of G) . x, createGraph ((the_Vertices_of G),(VertexAdjSymRel G)) & y2 Joins (the_Source_of G) . x,(the_Target_of G) . x, createGraph ((the_Vertices_of G),(VertexAdjSymRel G)) ) by GLIB_000:16;
then consider y0 being object such that
( y0 Joins (the_Source_of G) . x,(the_Target_of G) . x, createGraph ((the_Vertices_of G),(VertexAdjSymRel G)) & y0 in E9 ) and
A8: for y9 being object st y9 Joins (the_Source_of G) . x,(the_Target_of G) . x, createGraph ((the_Vertices_of G),(VertexAdjSymRel G)) & y9 in E9 holds
y9 = y0 by GLIB_009:def 5;
( y1 = y0 & y2 = y0 ) by A2, A6, A7, A8;
hence y1 = y2 ; :: thesis:

end;

suppose A9: ( y1 = [((the_Target_of G) . x),((the_Source_of G) . x)] & y2 = [((the_Source_of G) . x),((the_Target_of G) . x)] ) ; :: thesis:

end;

suppose ( y1 = [((the_Target_of G) . x),((the_Source_of G) . x)] & y2 = [((the_Target_of G) . x),((the_Source_of G) . x)] ) ; :: thesis:

hence y1 = y2 ; :: thesis:

end;

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

proof

per cases by A16, GLIB_000:16;

suppose z DJoins (the_Source_of G) . x,(the_Target_of G) . x, createGraph ((the_Vertices_of G),(VertexAdjSymRel G)) ; :: thesis:

hence S₁[x,z] by A15, A16, GLIB_000:def 21; :: thesis:

end;

suppose z DJoins (the_Target_of G) . x,(the_Source_of G) . x, createGraph ((the_Vertices_of G),(VertexAdjSymRel G)) ; :: thesis:

hence S₁[x,z] by A15, A16, GLIB_000:def 21; :: thesis:

end;

consider g being Function such that
A17: dom g = the_Edges_of G and
A18: for x being object st x in the_Edges_of G holds
S₁[x,g . x] from FUNCT_1:sch 2(A3, A13);

now :: thesis:

let y be object ; :: thesis:

hereby :: thesis:

assume y in rng g ; :: thesis:
then consider x being object such that
A19: ( x in dom g & g . x = y ) by FUNCT_1:def 3;
thus y in the_Edges_of G9 by A2, A17, A18, A19; :: thesis:

end;

assume A20: y in the_Edges_of G9 ; :: thesis:
set v = (the_Source_of G9) . y;
set w = (the_Target_of G9) . y;
y DJoins (the_Source_of G9) . y,(the_Target_of G9) . y,G9 by A20, GLIB_000:def 14;
then A21: y DJoins (the_Source_of G9) . y,(the_Target_of G9) . y, createGraph ((the_Vertices_of G),(VertexAdjSymRel G)) by GLIB_000:72;
then A22: y = [((the_Source_of G9) . y),((the_Target_of G9) . y)] by Th64;
then consider x being object such that
A23: x Joins (the_Source_of G9) . y,(the_Target_of G9) . y,G by A21, Th32, Th63;
A24: x in the_Edges_of G by A23, GLIB_000:def 13;

per cases ) . x = (the_Source_of G9) . y & (the_Target_of G) . x = (the_Target_of G9) . y ) or ( (the_Source_of G) . x = (the_Target_of G9) . y & (the_Target_of G) . x = (the_Source_of G9) . y ) ) by A23, GLIB_000:def 13;

suppose ( (the_Source_of G) . x = (the_Source_of G9) . y & (the_Target_of G) . x = (the_Target_of G9) . y ) ; :: thesis:

then A25: S₁[x,y] by A2, A20, A22;
S₁[x,g . x] by A18, A24;
then y = g . x by A3, A24, A25;
hence y in rng g by A17, A24, FUNCT_1:3; :: thesis:

end;

suppose ( (the_Source_of G) . x = (the_Target_of G9) . y & (the_Target_of G) . x = (the_Source_of G9) . y ) ; :: thesis:

then A26: S₁[x,y] by A2, A20, A22;
S₁[x,g . x] by A18, A24;
then y = g . x by A3, A24, A26;
hence y in rng g by A17, A24, FUNCT_1:3; :: thesis:

end;

then A27: rng g = the_Edges_of G9 by TARSKI:2;
then reconsider g = g as PartFunc of (the_Edges_of G),(the_Edges_of G9) by A17, RELSET_1:4;

now :: thesis:

thus for e being object st e in dom g holds
( (the_Source_of G) . e in dom f & (the_Target_of G) . e in dom f ) by FUNCT_2:5; :: thesis:
let e, v, w be object ; :: thesis:
assume A28: ( e in dom g & v in dom f & w in dom f & e Joins v,w,G ) ; :: thesis:
then A29: e in the_Edges_of G ;

per cases ) . e = v & (the_Target_of G) . e = w ) or ( (the_Source_of G) . e = w & (the_Target_of G) . e = v ) ) by A28, GLIB_000:def 13;

suppose A30: ( (the_Source_of G) . e = v & (the_Target_of G) . e = w ) ; :: thesis:

per cases by A18, A28;

suppose ( g . e in E9 & g . e = [((the_Source_of G) . e),((the_Target_of G) . e)] ) ; :: thesis:

then A31: g . e = [v,w] by A30;
g . e in rng g by A28, FUNCT_1:3;
then A32: g . e in the_Edges_of G9 ;
e Joins v,w,G by A30, A29, GLIB_000:def 13;
then [v,w] in VertexAdjSymRel G by Th32;
then ( g . e DJoins v,w, createGraph ((the_Vertices_of G),(VertexAdjSymRel G)) & v is set & w is set ) by A31, Th63, TARSKI:1;
then g . e DJoins v,w,G9 by A32, GLIB_000:73;
then g . e Joins v,w,G9 by GLIB_000:16;
then g . e Joins f . v,w,G9 by A28, FUNCT_1:18;
hence g . e Joins f . v,f . w,G9 by A28, FUNCT_1:18; :: thesis:

end;

suppose ( g . e in E9 & g . e = [((the_Target_of G) . e),((the_Source_of G) . e)] ) ; :: thesis:

then A33: g . e = [w,v] by A30;
g . e in rng g by A28, FUNCT_1:3;
then A34: g . e in the_Edges_of G9 ;
e Joins w,v,G by A30, A29, GLIB_000:def 13;
then ( g . e DJoins w,v, createGraph ((the_Vertices_of G),(VertexAdjSymRel G)) & v is set & w is set ) by A33, Th63, TARSKI:1, Th32;
then g . e DJoins w,v,G9 by A34, GLIB_000:73;
then g . e Joins v,w,G9 by GLIB_000:16;
then g . e Joins f . v,w,G9 by A28, FUNCT_1:18;
hence g . e Joins f . v,f . w,G9 by A28, FUNCT_1:18; :: thesis:

end;

suppose A35: ( (the_Source_of G) . e = w & (the_Target_of G) . e = v ) ; :: thesis:

per cases by A18, A28;

suppose ( g . e in E9 & g . e = [((the_Source_of G) . e),((the_Target_of G) . e)] ) ; :: thesis:

then A36: g . e = [w,v] by A35;
g . e in rng g by A28, FUNCT_1:3;
then A37: g . e in the_Edges_of G9 ;
e Joins w,v,G by A35, A29, GLIB_000:def 13;
then [w,v] in VertexAdjSymRel G by Th32;
then ( g . e DJoins w,v, createGraph ((the_Vertices_of G),(VertexAdjSymRel G)) & v is set & w is set ) by A36, Th63, TARSKI:1;
then g . e DJoins w,v,G9 by A37, GLIB_000:73;
then g . e Joins v,w,G9 by GLIB_000:16;
then g . e Joins f . v,w,G9 by A28, FUNCT_1:18;
hence g . e Joins f . v,f . w,G9 by A28, FUNCT_1:18; :: thesis:

end;

suppose ( g . e in E9 & g . e = [((the_Target_of G) . e),((the_Source_of G) . e)] ) ; :: thesis:

then A38: g . e = [v,w] by A35;
g . e in rng g by A28, FUNCT_1:3;
then A39: g . e in the_Edges_of G9 ;
e Joins v,w,G by A35, A29, GLIB_000:def 13;
then ( g . e DJoins v,w, createGraph ((the_Vertices_of G),(VertexAdjSymRel G)) & v is set & w is set ) by A38, Th63, TARSKI:1, Th32;
then g . e DJoins v,w,G9 by A39, GLIB_000:73;
then g . e Joins v,w,G9 by GLIB_000:16;
then g . e Joins f . v,w,G9 by A28, FUNCT_1:18;
hence g . e Joins f . v,f . w,G9 by A28, FUNCT_1:18; :: thesis:

end;

then reconsider F = [f,g] as PGraphMapping of G,G9 by GLIB_010:8;
take F ; :: thesis:

now :: thesis:

let x1, x2 be object ; :: thesis:
assume A40: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 ) ; :: thesis:

per cases by A18, A40;

suppose ( g . x1 = [((the_Source_of G) . x1),((the_Target_of G) . x1)] & g . x2 = [((the_Source_of G) . x2),((the_Target_of G) . x2)] ) ; :: thesis:

then ( (the_Source_of G) . x1 = (the_Source_of G) . x2 & (the_Target_of G) . x1 = (the_Target_of G) . x2 ) by A40, XTUPLE_0:1;
then ( x1 DJoins (the_Source_of G) . x1,(the_Target_of G) . x1,G & x2 DJoins (the_Source_of G) . x1,(the_Target_of G) . x1,G ) by A40, GLIB_000:def 14;
hence x1 = x2 by GLIB_000:def 21; :: thesis:

end;

suppose ( g . x1 = [((the_Source_of G) . x1),((the_Target_of G) . x1)] & g . x2 = [((the_Target_of G) . x2),((the_Source_of G) . x2)] ) ; :: thesis:

then ( (the_Source_of G) . x1 = (the_Target_of G) . x2 & (the_Target_of G) . x1 = (the_Source_of G) . x2 ) by A40, XTUPLE_0:1;
then ( x1 Joins (the_Source_of G) . x1,(the_Target_of G) . x1,G & x2 Joins (the_Source_of G) . x1,(the_Target_of G) . x1,G ) by A40, GLIB_000:def 13;
hence x1 = x2 by GLIB_000:def 20; :: thesis:

end;

suppose ( g . x1 = [((the_Target_of G) . x1),((the_Source_of G) . x1)] & g . x2 = [((the_Source_of G) . x2),((the_Target_of G) . x2)] ) ; :: thesis:

end;

suppose ( g . x1 = [((the_Target_of G) . x1),((the_Source_of G) . x1)] & g . x2 = [((the_Target_of G) . x2),((the_Source_of G) . x2)] ) ; :: thesis:

end;

then A41: g is one-to-one by FUNCT_1:def 4;
( f is one-to-one & F _V = f & F _E = g ) ;
then A42: F is one-to-one by A41, GLIB_010:def 13;
the_Vertices_of G = the_Vertices_of (createGraph ((the_Vertices_of G),(VertexAdjSymRel G)))
.= the_Vertices_of G9 by GLIB_000:def 33 ;
then A43: ( dom f = the_Vertices_of G & rng f = the_Vertices_of G9 ) ;
( F _V = f & F _E = g ) ;
then A44: ( F is total & F is onto ) by A17, A27, A43, GLIB_010:def 11, GLIB_010:def 12;
thus F is isomorphism by A42, A44; :: thesis:
thus F _V = id (the_Vertices_of G) ; :: thesis:
thus for e being object holds
( not e in the_Edges_of G or (F _E) . e = [((the_Source_of G) . e),((the_Target_of G) . e)] or (F _E) . e = [((the_Target_of G) . e),((the_Source_of G) . e)] ) by A18; :: thesis: