let V be non empty set ; :: thesis: for E being Relation of V
for Y being set holds Y |` E = (createGraph (V,E)) .edgesInto Y
let E be Relation of V; :: thesis: for Y being set holds Y |` E = (createGraph (V,E)) .edgesInto Y
let Y be set ; :: thesis: Y |` E = (createGraph (V,E)) .edgesInto Y
set G = createGraph (V,E);

now :: thesis: for z being object holds
( ( z in Y |` E implies z in (createGraph (V,E)) .edgesInto Y ) & ( z in (createGraph (V,E)) .edgesInto Y implies z in Y |` E ) )

let z be object ; :: thesis: ( ( z in Y |` E implies z in (createGraph (V,E)) .edgesInto Y ) & ( z in (createGraph (V,E)) .edgesInto Y implies z in Y |` E ) )

hereby :: thesis: ( z in (createGraph (V,E)) .edgesInto Y implies z in Y |` E )

assume A1: z in Y |` E ; :: thesis: z in (createGraph (V,E)) .edgesInto Y
then consider x, y being object such that
A2: z = [x,y] by RELAT_1:def 1;
A3: ( y in Y & [x,y] in E ) by A1, A2, RELAT_1:def 12;
then [x,y] DJoins x,y, createGraph (V,E) by Th63;
then ( [x,y] in the_Edges_of (createGraph (V,E)) & (the_Target_of (createGraph (V,E))) . [x,y] = y ) by GLIB_000:def 14;
hence z in (createGraph (V,E)) .edgesInto Y by A2, A3, GLIB_000:def 26; :: thesis: verum

end;

set x = (the_Source_of (createGraph (V,E))) . z;
set y = (the_Target_of (createGraph (V,E))) . z;
assume z in (createGraph (V,E)) .edgesInto Y ; :: thesis: z in Y |` E
then A4: ( z in the_Edges_of (createGraph (V,E)) & (the_Target_of (createGraph (V,E))) . z in Y ) by GLIB_000:def 26;
then z DJoins (the_Source_of (createGraph (V,E))) . z,(the_Target_of (createGraph (V,E))) . z, createGraph (V,E) by GLIB_000:def 14;
then z = [((the_Source_of (createGraph (V,E))) . z),((the_Target_of (createGraph (V,E))) . z)] by Th64;
hence z in Y |` E by A4, RELAT_1:def 12; :: thesis: verum

end;

hence Y |` E = (createGraph (V,E)) .edgesInto Y by TARSKI:2; :: thesis: verum