1 |-> r is Element of REAL 1 ;
hence <*r*> is Element of REAL 1 by FINSEQ_2:59; :: thesis: verum