now :: thesis: for x being object st x in dom (meet (the_Source_of S)) holds
x in meet (the_Edges_of S)

let x be object ; :: thesis: ( x in dom (meet (the_Source_of S)) implies x in meet (the_Edges_of S) )
assume A1: x in dom (meet (the_Source_of S)) ; :: thesis: x in meet (the_Edges_of S)

now :: thesis: for E being set st E in the_Edges_of S holds
x in E

let E be set ; :: thesis: ( E in the_Edges_of S implies x in E )
assume E in the_Edges_of S ; :: thesis: x in E
then consider G being _Graph such that
A2: ( G in S & E = the_Edges_of G ) by Def15;
A3: the_Source_of G in the_Source_of S by A2;
[x,((meet (the_Source_of S)) . x)] in meet (the_Source_of S) by A1, FUNCT_1:1;
then [x,((meet (the_Source_of S)) . x)] in the_Source_of G by A3, SETFAM_1:def 1;
then x in dom (the_Source_of G) by FUNCT_1:1;
hence x in E by A2; :: thesis: verum

end;

hence x in meet (the_Edges_of S) by SETFAM_1:def 1; :: thesis: verum

end;

hence meet (the_Source_of S) is meet (the_Edges_of S) -defined by TARSKI:def 3, RELAT_1:def 18; :: thesis: meet (the_Source_of S) is meet (the_Vertices_of S) -valued

now :: thesis: for y being object st y in rng (meet (the_Source_of S)) holds
y in meet (the_Vertices_of S)

let y be object ; :: thesis: ( y in rng (meet (the_Source_of S)) implies y in meet (the_Vertices_of S) )
assume y in rng (meet (the_Source_of S)) ; :: thesis: y in meet (the_Vertices_of S)
then consider x being object such that
A4: ( x in dom (meet (the_Source_of S)) & (meet (the_Source_of S)) . x = y ) by FUNCT_1:def 3;

now :: thesis: for V being set st V in the_Vertices_of S holds
y in V

let V be set ; :: thesis: ( V in the_Vertices_of S implies y in V )
assume V in the_Vertices_of S ; :: thesis: y in V
then consider G being _Graph such that
A5: ( G in S & V = the_Vertices_of G ) by Def14;
A6: the_Source_of G in the_Source_of S by A5;
[x,y] in meet (the_Source_of S) by A4, FUNCT_1:1;
then [x,y] in the_Source_of G by A6, SETFAM_1:def 1;
then ( x in dom (the_Source_of G) & (the_Source_of G) . x = y ) by FUNCT_1:1;
then y in rng (the_Source_of G) by FUNCT_1:3;
hence y in V by A5; :: thesis: verum

end;

hence y in meet (the_Vertices_of S) by SETFAM_1:def 1; :: thesis: verum

end;

hence meet (the_Source_of S) is meet (the_Vertices_of S) -valued by TARSKI:def 3, RELAT_1:def 19; :: thesis: verum