let p be Element of (TOP-REAL n); :: thesis: p is REAL -valued
let y be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not y in rng p or y in REAL )
assume y in rng p ; :: thesis: y in REAL
hence y in REAL by XREAL_0:def 1; :: thesis: verum