now :: thesis:

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

now :: thesis:

let E be set ; :: thesis:
assume E in the_Edges_of S ; :: thesis:
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:

end;

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

end;

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

now :: thesis:

let y be object ; :: thesis:
assume y in rng (meet (the_Source_of S)) ; :: thesis:
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:

let V be set ; :: thesis:
assume V in the_Vertices_of S ; :: thesis:
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:

end;

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

end;

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