let V1 be non empty set ; :: thesis:
let V2 be non empty Subset of V1; :: thesis:
let E1 be symmetric Relation of V1; :: thesis:
let E2 be symmetric Relation of V2; :: thesis:
let G1 be GraphFromSymRel of V1,E1; :: thesis:
let G2 be GraphFromSymRel of V2,E2; :: thesis:
assume A1: E2 c= E1 ; :: thesis:
set G3 = createGraph (V1,E1);
set G4 = createGraph (V2,E2);
set f = id V2;
( the_Vertices_of G1 = the_Vertices_of (createGraph (V1,E1)) & the_Vertices_of G2 = the_Vertices_of (createGraph (V2,E2)) ) by GLIB_000:def 33;
then A2: ( the_Vertices_of G1 = V1 & the_Vertices_of G2 = V2 ) ;
then ( dom (id V2) = the_Vertices_of G2 & rng (id V2) c= the_Vertices_of G1 ) ;
then reconsider f = id V2 as PartFunc of (the_Vertices_of G2),(the_Vertices_of G1) by RELSET_1:4;
defpred S₁[ object , object ] means ex v, w being object st
( $1 = [v,w] & $2 in the_Edges_of G1 & ( $2 = [v,w] or $2 = [w,v] ) );
A3: for x, y1, y2 being object st x in the_Edges_of G2 & S₁[x,y1] & S₁[x,y2] holds
y1 = y2

proof

let x, y1, y2 be object ; :: thesis:
assume A4: ( x in the_Edges_of G2 & S₁[x,y1] & S₁[x,y2] ) ; :: thesis:
then consider v, w being object such that
A5: ( x = [v,w] & y1 in the_Edges_of G1 & ( y1 = [v,w] or y1 = [w,v] ) ) ;
consider v0, w0 being object such that
A6: ( x = [v0,w0] & y2 in the_Edges_of G1 & ( y2 = [v0,w0] or y2 = [w0,v0] ) ) by A4;
A7: ( v = v0 & w = w0 ) by A5, A6, XTUPLE_0:1;

per cases by A5, A6, A7;

suppose ( y1 = [v,w] & y2 = [v,w] ) ; :: thesis:

hence y1 = y2 ; :: thesis:

end;

suppose A8: ( y1 = [v,w] & y2 = [w,v] ) ; :: thesis:

( y1 in E1 & y2 in E1 ) by A5, A6;
then A9: ( y1 DJoins v,w, createGraph (V1,E1) & y2 DJoins w,v, createGraph (V1,E1) ) by A8, Th63;
createGraph (V1,E1) is Supergraph of G1 by GLIB_006:57;
then ( y1 DJoins v,w,G1 & y2 DJoins w,v,G1 ) by A5, A6, A9, GLIB_006:71;
then ( y1 Joins v,w,G1 & y2 Joins v,w,G1 ) by GLIB_000:16;
hence y1 = y2 by GLIB_000:def 20; :: thesis:

end;

suppose A10: ( y1 = [w,v] & y2 = [v,w] ) ; :: thesis:

( y1 in E1 & y2 in E1 ) by A5, A6;
then A11: ( y1 DJoins w,v, createGraph (V1,E1) & y2 DJoins v,w, createGraph (V1,E1) ) by A10, Th63;
createGraph (V1,E1) is Supergraph of G1 by GLIB_006:57;
then ( y1 DJoins w,v,G1 & y2 DJoins v,w,G1 ) by A5, A6, A11, GLIB_006:71;
then ( y1 Joins v,w,G1 & y2 Joins v,w,G1 ) by GLIB_000:16;
hence y1 = y2 by GLIB_000:def 20; :: thesis:

end;

suppose ( y1 = [w,v] & y2 = [w,v] ) ; :: thesis:

hence y1 = y2 ; :: thesis:

end;

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

proof

let x be object ; :: thesis:
assume x in the_Edges_of G2 ; :: thesis:
then A13: x in E2 ;
then consider v, w being object such that
A14: x = [v,w] by RELAT_1:def 1;

per cases DJoins v,w,G1 or [w,v] DJoins w,v,G1 ) by A1, A13, A14, Th88;

suppose A15: [v,w] DJoins v,w,G1 ; :: thesis:

take [v,w] ; :: thesis:
take v ; :: thesis:
take w ; :: thesis:
thus ( x = [v,w] & [v,w] in the_Edges_of G1 & ( [v,w] = [v,w] or [v,w] = [w,v] ) ) by A14, A15, GLIB_000:def 14; :: thesis:

end;

suppose A16: [w,v] DJoins w,v,G1 ; :: thesis:

take [w,v] ; :: thesis:
take v ; :: thesis:
take w ; :: thesis:
thus ( x = [v,w] & [w,v] in the_Edges_of G1 & ( [w,v] = [v,w] or [w,v] = [w,v] ) ) by A14, A16, GLIB_000:def 14; :: thesis:

end;

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

now :: thesis:

let y be object ; :: 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;
consider v, w being object such that
A20: ( x = [v,w] & y in the_Edges_of G1 & ( y = [v,w] or y = [w,v] ) ) by A17, A18, A19;
thus y in the_Edges_of G1 by A20; :: thesis:

end;

then rng g c= the_Edges_of G1 by TARSKI:def 3;
then reconsider g = g as PartFunc of (the_Edges_of G2),(the_Edges_of G1) by A17, RELSET_1:4;

now :: thesis:

hereby :: thesis:

let e be object ; :: thesis:
assume e in dom g ; :: thesis:
then e Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G2 by GLIB_000:def 13;
hence ( (the_Source_of G2) . e in dom f & (the_Target_of G2) . e in dom f ) by A2, GLIB_000:13; :: thesis:

end;

let e, v, w be object ; :: thesis:
assume A21: ( e in dom g & v in dom f & w in dom f ) ; :: thesis:
assume A22: e Joins v,w,G2 ; :: thesis:
consider v0, w0 being object such that
A23: ( e = [v0,w0] & g . e in the_Edges_of G1 ) and
A24: ( g . e = [v0,w0] or g . e = [w0,v0] ) by A18, A21;
e in E2 by A21, TARSKI:def 3;
then e DJoins v0,w0, createGraph (V2,E2) by A23, Th63;
then A25: e Joins v0,w0, createGraph (V2,E2) by GLIB_000:16;
A26: ( e in the_Edges_of G2 & e is set & v is set & w is set ) by A21;
then e Joins v,w, createGraph (V2,E2) by A22, GLIB_000:72;
then ( ( v = v0 & w = w0 ) or ( v = w0 & w = v0 ) ) by A25, GLIB_000:15;

per cases by A24;

suppose A27: g . e = [v,w] ; :: thesis:

g . e in E1 by A23;
then g . e DJoins v,w, createGraph (V1,E1) by A27, Th63;
then g . e DJoins v,w,G1 by A23, A26, GLIB_000:73;
then g . e Joins v,w,G1 by GLIB_000:16;
then g . e Joins v,f . w,G1 by A21, FUNCT_1:18;
hence g . e Joins f . v,f . w,G1 by A21, FUNCT_1:18; :: thesis:

end;

suppose A28: g . e = [w,v] ; :: thesis:

g . e in E1 by A23;
then g . e DJoins w,v, createGraph (V1,E1) by A28, Th63;
then g . e DJoins w,v,G1 by A23, A26, GLIB_000:73;
then g . e Joins v,w,G1 by GLIB_000:16;
then g . e Joins v,f . w,G1 by A21, FUNCT_1:18;
hence g . e Joins f . v,f . w,G1 by A21, FUNCT_1:18; :: thesis:

end;

then reconsider F = [f,g] as PGraphMapping of G2,G1 by GLIB_010:8;
take F ; :: thesis:
for x1, x2 being object st x1 in dom g & x2 in dom g & g . x1 = g . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis:
assume A29: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 ) ; :: thesis:
then consider v1, w1 being object such that
A30: ( x1 = [v1,w1] & g . x1 in the_Edges_of G1 ) and
A31: ( g . x1 = [v1,w1] or g . x1 = [w1,v1] ) by A18;
consider v2, w2 being object such that
A32: ( x2 = [v2,w2] & g . x2 in the_Edges_of G1 ) and
A33: ( g . x2 = [v2,w2] or g . x2 = [w2,v2] ) by A18, A29;

per cases by A31, A33;

suppose ( ( g . x1 = [v1,w1] & g . x2 = [v2,w2] ) or ( g . x1 = [w1,v1] & g . x2 = [w2,v2] ) ) ; :: thesis:

then ( v1 = v2 & w1 = w2 ) by A29, XTUPLE_0:1;
hence x1 = x2 by A30, A32; :: thesis:

end;

suppose ( ( g . x1 = [v1,w1] & g . x2 = [w2,v2] ) or ( g . x1 = [w1,v1] & g . x2 = [v2,w2] ) ) ; :: thesis:

then A34: ( v1 = w2 & w1 = v2 ) by A29, XTUPLE_0:1;
( x1 in E2 & x2 in E2 ) by A29, TARSKI:def 3;
then A35: ( x1 DJoins v1,w1, createGraph (V2,E2) & x2 DJoins w1,v1, createGraph (V2,E2) ) by A30, A32, A34, Th63;
( x1 in the_Edges_of G2 & x2 in the_Edges_of G2 & x1 is set & x2 is set & v1 is set & w1 is set ) by A29, TARSKI:1;
then ( x1 DJoins v1,w1,G2 & x2 DJoins w1,v1,G2 ) by A35, GLIB_000:73;
then ( x1 Joins v1,w1,G2 & x2 Joins v1,w1,G2 ) by GLIB_000:16;
hence x1 = x2 by GLIB_000:def 20; :: thesis:

end;

then A36: F _E is one-to-one by FUNCT_1:def 4;
F _V is one-to-one ;
then A37: F is one-to-one by A36, GLIB_010:def 13;
( dom (F _V) = the_Vertices_of G2 & dom (F _E) = the_Edges_of G2 ) by A2, A17;
then F is total by GLIB_010:def 11;
hence F is weak_SG-embedding by A37; :: thesis:
thus F _V = id V2 ; :: thesis:
let v, w be object ; :: thesis:
assume [v,w] in the_Edges_of G2 ; :: thesis:
then consider v0, w0 being object such that
A38: ( [v,w] = [v0,w0] & g . [v,w] in the_Edges_of G1 ) and
A39: ( g . [v,w] = [v0,w0] or g . [v,w] = [w0,v0] ) by A18;
( v = v0 & w = w0 ) by A38, XTUPLE_0:1;
hence ( (F _E) . [v,w] = [v,w] or (F _E) . [v,w] = [w,v] ) by A39; :: thesis: