let R be SubSpace of T; :: thesis: R is real-membered
the carrier of R is real-membered

proof

let x be set ; :: according to MEMBERED:def 3 :: thesis: ( not x in the carrier of R or x is real )
A1: the carrier of R c= the carrier of T by BORSUK_1:35;
assume x in the carrier of R ; :: thesis: x is real
hence x is real by A1; :: thesis: verum

end;

hence R is real-membered by BORSUK_4:def 2; :: thesis: verum