for F being ext-real-membered set
for f being ExtReal
for e being set st e in F /// f holds
ex w being Element of ExtREAL st
( e = w / f & w in F )