now :: thesis: for x being object st x in the carrier of FMT_R^1 holds
x is real
let x be object ; :: thesis: ( x in the carrier of FMT_R^1 implies x is real )
assume x in the carrier of FMT_R^1 ; :: thesis: x is real
then reconsider x9 = x as Element of FMT_R^1 ;
x9 in the carrier of (Top2NTop R^1) ;
then x in the carrier of R^1 by FINTOPO7:def 15;
hence x is real ; :: thesis: verum
end;
hence FMT_R^1 is real-membered by TOPMETR:def 8, MEMBERED:def 3; :: thesis: verum