theorem :: MEMBER_1:111

for f, g being ExtReal holds {f} /// {g} = {(f / g)}