let A be SubSpace of S; :: thesis: A is real-functions-membered
let x be object ; :: according to VALUED_2:def 4,TOPREALC:def 2 :: thesis: ( not x in the carrier of A or x is set )
the carrier of A c= the carrier of S by BORSUK_1:1;
hence ( not x in the carrier of A or x is set ) ; :: thesis: verum