let V be non empty set ; for E being Relation of V
for X being set holds E | X = (createGraph (V,E)) .edgesOutOf X
let E be Relation of V; for X being set holds E | X = (createGraph (V,E)) .edgesOutOf X
let X be set ; E | X = (createGraph (V,E)) .edgesOutOf X
set G = createGraph (V,E);
now 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 ;
( ( 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 ( z in (createGraph (V,E)) .edgesOutOf X implies z in E | X )
assume A1:
z in E | X
;
z in (createGraph (V,E)) .edgesOutOf Xthen 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;
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
;
z in E | Xthen 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;
verum end;
hence
E | X = (createGraph (V,E)) .edgesOutOf X
by TARSKI:2; verum