defpred S₁[ set ] means ( $1 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G & ( for e2 being set st e2 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G holds
((L `1) . ((the_Source_of G) . $1)) + ((the_Weight_of G) . $1) <= ((L `1) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) );
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 e1 being set holds
( e1 in IT iff ( e1 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G & ( for e2 being set st e2 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G holds
((L `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) )

now

let e1 be set ; :: thesis: ( ( e1 in IT implies S₁[e1] ) & ( S₁[e1] implies e1 in IT ) )
thus ( e1 in IT implies S₁[e1] ) by A1; :: thesis: ( S₁[e1] implies e1 in IT )
assume A2: S₁[e1] ; :: thesis: e1 in IT
then e1 in the_Edges_of G by GLIB_000:def 16;
hence e1 in IT by A1, A2; :: thesis: verum

end;

hence for e1 being set holds
( e1 in IT iff ( e1 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G & ( for e2 being set st e2 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G holds
((L `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) ) ; :: thesis: verum