let X be non empty ext-real-membered set ; :: thesis: ex e being ext-real number st e in X
ex x being set st x in X by XBOOLE_0:def 1;
hence ex e being ext-real number st e in X ; :: thesis: verum