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

now :: thesis: for z being object holds
( ( z in E | X implies z in (createGraph (V,E)) .edgesOutOf X ) & ( z in (createGraph (V,E)) .edgesOutOf X implies z in E | X ) )

let z be object ; :: thesis: ( ( z in E | X implies z in (createGraph (V,E)) .edgesOutOf X ) & ( z in (createGraph (V,E)) .edgesOutOf X implies z in E | X ) )

hereby :: thesis: ( z in (createGraph (V,E)) .edgesOutOf X implies z in E | X )

assume A1: z in E | X ; :: thesis: z in (createGraph (V,E)) .edgesOutOf X
then consider x, y being object such that
A2: z = [x,y] by RELAT_1:def 1;
A3: ( x in X & [x,y] in E ) by A1, A2, RELAT_1:def 11;
then [x,y] DJoins x,y, createGraph (V,E) by Th63;
then ( [x,y] in the_Edges_of (createGraph (V,E)) & (the_Source_of (createGraph (V,E))) . [x,y] = x ) by GLIB_000:def 14;
hence z in (createGraph (V,E)) .edgesOutOf X by A2, A3, GLIB_000:def 27; :: 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)) .edgesOutOf X ; :: thesis: z in E | X
then A4: ( z in the_Edges_of (createGraph (V,E)) & (the_Source_of (createGraph (V,E))) . z in X ) by GLIB_000:def 27;
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 E | X by A4, RELAT_1:def 11; :: thesis: verum

end;

hence E | X = (createGraph (V,E)) .edgesOutOf X by TARSKI:2; :: thesis: verum