let X be set ; :: thesis: for f being PartFunc of REAL,REAL st f is_strongly_quasiconvex_on X holds
f is_strictly_quasiconvex_on X
let f be PartFunc of REAL,REAL; :: thesis: ( f is_strongly_quasiconvex_on X implies f is_strictly_quasiconvex_on X )
assume f is_strongly_quasiconvex_on X ; :: thesis: f is_strictly_quasiconvex_on X
then ( X c= dom f & ( for p being Real st 0 < p & p < 1 holds
for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & f . r <> f . s holds
f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ) ) by Def4;
hence f is_strictly_quasiconvex_on X by Def3; :: thesis: verum