E-min (L~ g) in rng g by SPRECT_2:45;
hence ex b₁ being Nat st
( 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = E-min (L~ g) ) by Th3; :: thesis: verum