let X be non empty real-membered set ; :: thesis: ex r being real number st r in X
consider x being set such that
A1: x in X by XBOOLE_0:def 1;
thus ex r being real number st r in X by A1; :: thesis: verum