let a be Element of (Euclid n); :: thesis: a is REAL -valued

let y be object ; :: according to RELAT_1:def 19,TARSKI:def 3 :: thesis: ( not y in rng 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

let y be object ; :: according to RELAT_1:def 19,TARSKI:def 3 :: thesis: ( not y in rng 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