defpred S1[ 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 & S1[e] ) )
from SUBSET_1:sch 1();
take
IT
; 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 for e1 being set holds
( ( e1 in IT implies S1[e1] ) & ( S1[e1] implies e1 in IT ) )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) ) ) )
; verum