theorem Th15: :: FUZZY_6:14

for f, g being Function of REAL,REAL holds max (f,g) = (1 / 2) (#) ((f + g) + (abs (f - g)))