let x be object ; :: thesis: ( x in dom (union (the_Source_of S)) implies x in union (the_Edges_of S) )
set y = (union (the_Source_of S)) . x;
assume x in dom (union (the_Source_of S)) ; :: thesis: x in union (the_Edges_of S)
then [x,((union (the_Source_of S)) . x)] in union (the_Source_of S) by FUNCT_1:1;
then consider s being set such that
A1: ( [x,((union (the_Source_of S)) . x)] in s & s in the_Source_of S ) by TARSKI:def 4;
consider G being _Graph such that
A2: ( G in S & s = the_Source_of G ) by A1, Def16;
x in dom (the_Source_of G) by A1, A2, FUNCT_1:1;
then A3: x in the_Edges_of G ;
the_Edges_of G in the_Edges_of S by A2, Def15;
hence x in union (the_Edges_of S) by A3, TARSKI:def 4; :: thesis: verum

let y be object ; :: thesis: ( y in rng (union (the_Source_of S)) implies y in union (the_Vertices_of S) )
assume y in rng (union (the_Source_of S)) ; :: thesis: y in union (the_Vertices_of S)
then consider x being object such that
A4: ( x in dom (union (the_Source_of S)) & (union (the_Source_of S)) . x = y ) by FUNCT_1:def 3;
[x,y] in union (the_Source_of S) by A4, FUNCT_1:1;
then consider s being set such that
A5: ( [x,y] in s & s in the_Source_of S ) by TARSKI:def 4;
consider G being _Graph such that
A6: ( G in S & s = the_Source_of G ) by A5, Def16;
A7: x in dom (the_Source_of G) by A5, A6, FUNCT_1:1;
then (the_Source_of G) . x = y by A4, A5, A6, COMPUT_1:13;
then y in rng (the_Source_of G) by A7, FUNCT_1:3;
then A8: y in the_Vertices_of G ;
the_Vertices_of G in the_Vertices_of S by A6, Def14;
hence y in union (the_Vertices_of S) by A8, TARSKI:def 4; :: thesis: verum