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

let x be object ; :: thesis: ( x in meet (the_Edges_of S) implies x in dom (meet (the_Source_of S)) )
assume A1: x in meet (the_Edges_of S) ; :: thesis: x in dom (meet (the_Source_of S))
set G0 = the Element of S;
set y = (the_Source_of the Element of S) . x;

now :: thesis: for s being set st s in the_Source_of S holds
[x,((the_Source_of the Element of S) . x)] in s

let s be set ; :: thesis: ( s in the_Source_of S implies [x,((the_Source_of the Element of S) . x)] in s )
assume s in the_Source_of S ; :: thesis: [x,((the_Source_of the Element of S) . x)] in s
then consider G being _Graph such that
A2: ( G in S & s = the_Source_of G ) by Def16;
the_Edges_of G in the_Edges_of S by A2;
then x in the_Edges_of G by A1, SETFAM_1:def 1;
then A3: x in dom (the_Source_of G) by FUNCT_2:def 1;
then A4: [x,((the_Source_of G) . x)] in the_Source_of G by FUNCT_1:1;
the_Edges_of the Element of S in the_Edges_of S ;
then x in the_Edges_of the Element of S by A1, SETFAM_1:def 1;
then x in dom (the_Source_of the Element of S) by FUNCT_2:def 1;
then A5: x in (dom (the_Source_of the Element of S)) /\ (dom (the_Source_of G)) by A3, XBOOLE_0:def 4;
G tolerates the Element of S by A2, Def27;
then the_Source_of G tolerates the_Source_of the Element of S ;
hence [x,((the_Source_of the Element of S) . x)] in s by A2, A4, A5, PARTFUN1:def 4; :: thesis: verum

end;

then [x,((the_Source_of the Element of S) . x)] in meet (the_Source_of S) by SETFAM_1:def 1;
hence x in dom (meet (the_Source_of S)) by FUNCT_1:1; :: thesis: verum

end;

then meet (the_Edges_of S) c= dom (meet (the_Source_of S)) by TARSKI:def 3;
hence meet (the_Source_of S) is total by PARTFUN1:def 2, XBOOLE_0:def 10; :: thesis: verum