thus the carrier of RealSpace is real-membered ; :: according to TOPMETR:def 9 :: thesis: verum