reconsider p = r as Element of REAL by XREAL_0:def 1;
<*p*> is FinSequence-like ;
hence <*r*> is real-valued ; :: thesis: verum