let X be set ; :: thesis: ( X is rational-membered implies X is real-membered )
assume A3: X is rational-membered ; :: thesis: X is real-membered
let x be object ; :: according to MEMBERED:def 3 :: thesis: ( x in X implies x is real )
assume x in X ; :: thesis: x is real
then x is rational by A3;
then x in RAT ;
hence x in REAL by NUMBERS:12; :: according to XREAL_0:def 1 :: thesis: verum