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 by METRIC_1:def 14; :: according to BORSUK_4:def 2 :: thesis: verum