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 ) );
consider IT being Subset of (the_Edges_of G) such that
A1: for e1 being set holds
( e1 in IT iff ( e1 in the_Edges_of G & S₁[e1] ) ) from SUBSET_1:sch 1();
take IT ; :: thesis: for e1 being set holds
( e1 in IT 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 ) ) )
let e1 be set ; :: thesis: ( e1 in IT 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 ) ) )
thus ( e1 in IT implies S₁[e1] ) by A1; :: thesis: ( 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 e1 in IT )
assume A2: S₁[e1] ; :: thesis: e1 in IT
then e1 in the_Edges_of G by GLIB_000:def 15;
hence e1 in IT by A1, A2; :: thesis: verum