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