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