Voilà où j'en suis, mais peut-être fais-je fausse route.

Notons Jo=[s,t]. Supposons f(s) < f(t).

Notons J1=[c,d]

Il me semble que si l'on prend  b = le plus petit antécédent de  d  par  f  appartenant à  J0  et  a  le plus grand antécédent de  c  par  f  plus petit que  b  alors  J'0=[a,b]  devrait convenir.

Il reste à vérifier si a et b sont bien définis et si [a,b] convient (il reste tout à vérifier quoi )

Plus j'y pense plus ça m'a l'air juste

oui c'est juste à une condition : démontrer que le plus grand antécédent existe ...

On veut prouver qu'il existe c', d'  tels que [s',t] c  [s,t] et [c,d] = f<[s',t']>

il faut dire que l'ensemble f^-1 {c} est non vide, majoré par b donc possède un sup
et il existe une suite (un) d'éléments de f-1{c} convergent vers ce sup, et f(un) = c donc et f continue en ce sup, on a f(sup=alpha) = c donc le sup est un max.
et la tu as bien ton plus grand élément..

après il reste quand meme a distinguer les cas

soit A ={  x  dans [alpha,b],  f(x) = d} si cet ensemble n'est pas vide, on montre qu'il a un plus petit élément beta, et J1 c f([alpha,beta]),
L'inclusion inverse , on peut la prouver par l'absurde: soit x dans (alpha,beta) tel que f(x) n'est pas dans J1,
si f(x) > d, le TVI nous fournit un autre xo dans (alpha;x) antécédent de d ce qui est absurde car xo < beta.
si f(x) < c on trouve de la meme maniere une absurdité
On a donc l'inclusion inverse donc l'égalité.

SI A est vide, on considere B = {x dans (0,alpha)/ f(x)=d} non vide ... et on raisonne de meme

on abien trouvé lensemble

Pour justifier que le plus grand antécédent existe, tu peux dire que est fermé car image réciproque d'un fermé par f continue donc fermé borné il possède un max.

oui exact