defpred S1[ set ] means ( \$1 DSJoins dom (L `1),() \ (dom (L `1)),G & ( for e2 being set st e2 DSJoins dom (L `1),() \ (dom (L `1)),G holds
((L `1) . (() . \$1)) + (() . \$1) <= ((L `1) . (() . e2)) + (() . e2) ) );
consider IT being Subset of () such that
A1: for e being set holds
( e in IT iff ( e in the_Edges_of G & S1[e] ) ) from take IT ; :: thesis: for e1 being set holds
( e1 in IT iff ( e1 DSJoins dom (L `1),() \ (dom (L `1)),G & ( for e2 being set st e2 DSJoins dom (L `1),() \ (dom (L `1)),G holds
((L `1) . (() . e1)) + (() . e1) <= ((L `1) . (() . e2)) + (() . e2) ) ) )

now :: thesis: for e1 being set holds
( ( e1 in IT implies S1[e1] ) & ( S1[e1] implies e1 in IT ) )
let e1 be set ; :: thesis: ( ( e1 in IT implies S1[e1] ) & ( S1[e1] implies e1 in IT ) )
thus ( e1 in IT implies S1[e1] ) by A1; :: thesis: ( S1[e1] implies e1 in IT )
assume A2: S1[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;
hence for e1 being set holds
( e1 in IT iff ( e1 DSJoins dom (L `1),() \ (dom (L `1)),G & ( for e2 being set st e2 DSJoins dom (L `1),() \ (dom (L `1)),G holds
((L `1) . (() . e1)) + (() . e1) <= ((L `1) . (() . e2)) + (() . e2) ) ) ) ; :: thesis: verum