let X be real-membered set ; :: thesis: ( ( for r being real number holds r in X ) implies X = REAL )
assume A1: for r being real number holds r in X ; :: thesis: X = REAL
thus X c= REAL by Th3; :: according to XBOOLE_0:def 10 :: thesis: REAL c= X
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in REAL or e in X )
assume e in REAL ; :: thesis: e in X
then e is real ;
hence e in X by A1; :: thesis: verum