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