for a, b, c being ExtReal st a <= c & b <= c & ( for d being ExtReal st a <= d & b <= d holds
c <= d ) holds
c = max (a,b)