let n be Nat; :: thesis: for f being Element of REAL * holds Argmin ((OuterVx (f,n)),f,n) <= n
let f be Element of REAL * ; :: thesis: Argmin ((OuterVx (f,n)),f,n) <= n
set IN = OuterVx (f,n);

per cases ( OuterVx (f,n) <> {} or OuterVx (f,n) = {} ) ;

suppose OuterVx (f,n) <> {} ; :: thesis: Argmin ((OuterVx (f,n)),f,n) <= n

hence Argmin ((OuterVx (f,n)),f,n) <= n by Th29; :: thesis: verum

end;

suppose OuterVx (f,n) = {} ; :: thesis: Argmin ((OuterVx (f,n)),f,n) <= n

hence Argmin ((OuterVx (f,n)),f,n) <= n by Def10; :: thesis: verum

end;

end;