now 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 ;
( 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)
;
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 for s being set st s in the_Source_of S holds
[x,((the_Source_of the Element of S) . x)] in slet s be
set ;
( 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
;
[x,((the_Source_of the Element of S) . x)] in sthen 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;
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;
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; verum