let T be SubSpace of RealSpace ; :: thesis: T is real-membered
the carrier of T is Subset of RealSpace by TOPMETR:def 1;
hence the carrier of T is real-membered ; :: according to TOPMETR:def 8 :: thesis: verum