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) ) );
let IT1, IT2 be Subset of (the_Edges_of G); :: thesis: ( ( for e1 being set holds
( e1 in IT1 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) ) ) ) ) & ( for e1 being set holds
( e1 in IT2 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) ) ) ) ) implies IT1 = IT2 )
assume that
A3: for y being set holds
( y in IT1 iff S1[y] ) and
A4: for y being set holds
( y in IT2 iff S1[y] ) ; :: thesis: IT1 = IT2
now :: thesis: for x being object holds
( ( x in IT1 implies x in IT2 ) & ( x in IT2 implies x in IT1 ) )
let x be object ; :: thesis: ( ( x in IT1 implies x in IT2 ) & ( x in IT2 implies x in IT1 ) )
reconsider xx = x as set by TARSKI:1;
hereby :: thesis: ( x in IT2 implies x in IT1 )
assume x in IT1 ; :: thesis: x in IT2
then S1[xx] by A3;
hence x in IT2 by A4; :: thesis: verum
end;
assume x in IT2 ; :: thesis: x in IT1
then S1[xx] by A4;
hence x in IT1 by A3; :: thesis: verum
end;
hence IT1 = IT2 by TARSKI:2; :: thesis: verum