defpred S₁[ set ] means (the_Target_of G) . $1 in X;
consider IT being Subset of (the_Edges_of G) such that
A1: 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_Target_of G) . e in X ) )
thus for e being set holds
( e in IT iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) by A1; :: thesis: verum