let R be SubSpace of T; :: thesis: R is real-membered
let x be set ; :: according to MEMBERED:def 3,TOPMETR:def 8 :: thesis: ( not x in the carrier of R or x is real )
the carrier of R c= the carrier of T by BORSUK_1:1;
hence ( not x in the carrier of R or x is real ) ; :: thesis: verum