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

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

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

let s be set ; :: thesis: ( s in the_Target_of S implies [x,((the_Target_of the Element of S) . x)] in s )
assume s in the_Target_of S ; :: thesis: [x,((the_Target_of the Element of S) . x)] in s
then consider G being _Graph such that
A7: ( G in S & s = the_Target_of G ) by Def17;
the_Edges_of G in the_Edges_of S by A7;
then x in the_Edges_of G by A6, SETFAM_1:def 1;
then A8: x in dom (the_Target_of G) by FUNCT_2:def 1;
then A9: [x,((the_Target_of G) . x)] in the_Target_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 A6, SETFAM_1:def 1;
then x in dom (the_Target_of the Element of S) by FUNCT_2:def 1;
then A10: x in (dom (the_Target_of the Element of S)) /\ (dom (the_Target_of G)) by A8, XBOOLE_0:def 4;
G tolerates the Element of S by A7, Def27;
then the_Target_of G tolerates the_Target_of the Element of S ;
hence [x,((the_Target_of the Element of S) . x)] in s by A7, A9, A10, PARTFUN1:def 4; :: thesis: verum

end;

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

end;

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