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

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