let X be set ; :: thesis: for f being PartFunc of REAL,REAL st f is_convex_on X holds
f is_strictly_quasiconvex_on X
let f be PartFunc of REAL,REAL; :: thesis: ( f is_convex_on X implies f is_strictly_quasiconvex_on X )
assume A1: f is_convex_on X ; :: thesis: f is_strictly_quasiconvex_on X
A2: 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))

proof

let p be Real; :: thesis: ( 0 < p & p < 1 implies 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)) )
assume that
A3: 0 < p and
A4: p < 1 ; :: thesis: 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))
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))

proof

let r, s be Real; :: thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X & f . r <> f . s implies f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) )
assume that
A5: ( r in X & s in X & (p * r) + ((1 - p) * s) in X ) and
A6: f . r <> f . s ; :: thesis: f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s))
A7: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) by A1, A3, A4, A5, RFUNCT_3:def 12;
A8: 1 - p > 0 by A4, XREAL_1:50;

now :: thesis: f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s))

per cases ( f . r < f . s or f . r > f . s ) by A6, XXREAL_0:1;

suppose f . r < f . s ; :: thesis: f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s))

then p * (f . r) < p * (f . s) by A3, XREAL_1:68;
then (p * (f . r)) + ((1 - p) * (f . s)) < (p * (f . s)) + ((1 - p) * (f . s)) by XREAL_1:6;
then A9: f . ((p * r) + ((1 - p) * s)) < f . s by A7, XXREAL_0:2;
f . s <= max ((f . r),(f . s)) by XXREAL_0:25;
hence f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) by A9, XXREAL_0:2; :: thesis: verum

end;

suppose f . r > f . s ; :: thesis: f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s))

then (1 - p) * (f . r) > (1 - p) * (f . s) by A8, XREAL_1:68;
then (p * (f . r)) + ((1 - p) * (f . s)) < (p * (f . r)) + ((1 - p) * (f . r)) by XREAL_1:6;
then A10: f . ((p * r) + ((1 - p) * s)) < f . r by A7, XXREAL_0:2;
f . r <= max ((f . r),(f . s)) by XXREAL_0:25;
hence f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) by A10, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ; :: thesis: verum

end;

hence 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)) ; :: thesis: verum

end;

X c= dom f by A1, RFUNCT_3:def 12;
hence f is_strictly_quasiconvex_on X by A2; :: thesis: verum