let FT be non empty RelStr ; :: thesis: for X9 being SubSpace of FT
for A being Subset of X9 holds A is Subset of FT
let X9 be SubSpace of FT; :: thesis: for A being Subset of X9 holds A is Subset of FT
let A be Subset of X9; :: thesis: A is Subset of FT
the carrier of X9 c= the carrier of FT by Def2;
hence A is Subset of FT by XBOOLE_1:1; :: thesis: verum