let r be Element of REAL ; :: thesis: r is real
thus r in REAL ; :: according to XREAL_0:def 1 :: thesis: verum