defpred S_{1}[ 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_{1}[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) ) ) )

( 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

((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

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 :: thesis: for e1 being set holds

( ( e1 in IT implies S_{1}[e1] ) & ( S_{1}[e1] implies e1 in IT ) )

hence
for e1 being set holds ( ( e1 in IT implies S

let e1 be set ; :: thesis: ( ( e1 in IT implies S_{1}[e1] ) & ( S_{1}[e1] implies e1 in IT ) )

thus ( e1 in IT implies S_{1}[e1] )
by A1; :: thesis: ( S_{1}[e1] implies e1 in IT )

assume A2: S_{1}[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;thus ( e1 in IT implies S

assume A2: S

then e1 in the_Edges_of G by GLIB_000:def 16;

hence e1 in IT by A1, A2; :: thesis: verum

( 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