theorem :: XXREAL_0:34

for a, b, c being ExtReal holds max ((max (a,b)),c) = max (a,(max (b,c)))