defpred S₁[ set ] means ( $1 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G holds
(the_Weight_of G) . $1 <= (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 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G holds
(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) ) ) & ( for e1 being set holds
( e1 in IT2 iff ( e1 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G holds
(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) ) ) implies IT1 = IT2 )
assume that
A3: for e1 being set holds
( e1 in IT1 iff ( e1 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G holds
(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) ) and
A4: for e1 being set holds
( e1 in IT2 iff ( e1 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G holds
(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) ) ; :: thesis: IT1 = IT2

now :: thesis: for e1 being object holds
( ( e1 in IT1 implies e1 in IT2 ) & ( e1 in IT2 implies e1 in IT1 ) )

let e1 be object ; :: thesis: ( ( e1 in IT1 implies e1 in IT2 ) & ( e1 in IT2 implies e1 in IT1 ) )
reconsider ee = e1 as set by TARSKI:1;

hereby :: thesis: ( e1 in IT2 implies e1 in IT1 )

assume e1 in IT1 ; :: thesis: e1 in IT2
then S₁[ee] by A3;
hence e1 in IT2 by A4; :: thesis: verum

end;

assume e1 in IT2 ; :: thesis: e1 in IT1
then S₁[ee] by A4;
hence e1 in IT1 by A3; :: thesis: verum

end;

hence IT1 = IT2 by TARSKI:2; :: thesis: verum