defpred S₁[ set ] means (the_Source_of G) . $1 in X;
consider IT being Subset of (the_Edges_of G) such that
A6: for e being set holds
( e in IT iff ( e in the_Edges_of G & S₁[e] ) ) from SUBSET_1:sch 1();
take IT ; :: thesis: for e being set holds
( e in IT iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) )
thus for e being set holds
( e in IT iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) by A6; :: thesis: verum