for x being Element of ExtREAL holds x |^ 1 = x