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