for X being ext-real-membered set st ( for e being ExtReal holds e in X ) holds
X = ExtREAL