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

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