:: deftheorem Def16 defines .tolerance GLIB_005:def 16 :
for G being natural-weighted WGraph
for EL being FF:ELabeling of G
for W being Walk of G st W is_augmenting_wrt EL holds
for b₄ being Nat holds
( ( W is V5() implies ( b₄ = W .tolerance EL iff ( b₄ in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds
b₄ <= k ) ) ) ) & ( W is V5() implies ( b₄ = W .tolerance EL iff b₄ = 0 ) ) );